Infinite sequence

Set

 context $X$
 definiendum $A\in \mathrm{InfSequence}(X)$
 postulate $A: \mathbb N\to X$

Discussion

Instead of $\langle n,A(n)\rangle$, we also write $A_n$ and denote the whole sequence by $(A_n)_{n\in\mathbb N}$ or just $(A_n)$.