Subsequences

In the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, let $(a_{n})$ be a sequence in a set $X$, that is a map $a:\mathbb{N}\to X$, and let $\mathbb{N}$ carry its order $\le$ of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §order, a total order with strict relation $<$ by Arithmetic and Order of the Natural Numbers §partial-order and Arithmetic and Order of the Natural Numbers §trichotomy.

¶ A subsequence of $(a_{n})$ is a sequence $a\circ\sigma=(a_{\sigma(k)})_{k\in\mathbb{N}}$, where $\sigma:\mathbb{N}\to\mathbb{N}$ is a strictly increasing sequence in $\mathbb{N}$.