Proof of Sequences: Enlarging the Codomain, Extensionality and the Range

The "in particular" readings follow because a sequence in a set $X$ is a map $\mathbb{N}\to X$ whose $n$-th term is its value at $n$ (Sequences (i)).

Proof of (i). Let $A\subseteq B$ and let $a:\mathbb{N}\to A$ be a map. Every value $a(n)$ lies in $A$ (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (i)), hence in $B$, so $a:\mathbb{N}\to B$ is a map by Membership in Inverse Relations, Preimages and Images of Classes, and Enlarging the Codomain of a Map (v), applied to $F=a$ with domain $\mathbb{N}$, codomain $A$ and $D=B$.

Proof of (ii). The maps $a$ and $b$ have the same domain $\mathbb{N}$ and equal values at every $k\in\mathbb{N}$, so $b=a$ by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii), applied to $F=a$ and $G=b$ with both codomains $X$.

Proof of (iii). Let $a:\mathbb{N}\to X$ be a map and $y$ a class. By Relations, Domain, Range, Inverse and Composition (iii) and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i), a set $v$ lies in $\operatorname{ran}a$ if and only if $(u,v)\in a$ for some set $u$.

Suppose $y\in\operatorname{ran}a$. Then (as an element of a class, $y$ is a set by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (i)) there is a set $n$ with $(n,y)\in a$. By Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ii), this gives $n\in\mathbb{N}$ and $y=a(n)=a_{n}$.

Conversely, let $n\in\mathbb{N}$ with $y=a_{n}$. By Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (i), $a(n)$ is a set and $(n,a(n))\in a$, so $a(n)\in\operatorname{ran}a$ by the description of the range above; that is, $y\in\operatorname{ran}a$.