DEF-SEQ-T. Transfinite Sequence.
A transfinite sequence is a function whose domain is an ordinal.
If $s:\alpha\to X$ be a transfinite sequence for some ordinal $\alpha$:
$s$ is called a transfinite sequence in $X$.
$\alpha$ is called the length of $s$; $s$ an $\alpha$-sequence.
$s$ is also denoted by
\[\langle s_\xi : \xi<\alpha\rangle \quad\text{or}\quad \langle s_\xi\rangle_{\xi<\alpha},\]where $s_\xi$ stands for $s(\xi)$.
An infinite sequence is an $\omega$-sequence.
An infinite sequence $s$ is also denoted by
\[\langle s_n : n\in\N\rangle \quad\text{or}\quad \langle s_n\rangle_{n\in\N}.\]
A finite sequence is an $n$-sequence for some natural number $n$.
If $s$ is an $\alpha$-sequence, the extension of $s$ by $x$ is
\[s^\frown x = s\cup\{(\alpha,x)\}.\]