Proof of Evaluating a Sequence of Maps at a Point Gives a Sequence, and Its Range

Proof of (i). The sequence $(f_{m})$ is a map $f:\mathbb{N}\to Y^{X}$ with $f(m)=f_{m}$ (Sequences (i)). Let $c:\mathbb{N}\to X$ be the map with $c(m)=x$ for every $m\in\mathbb{N}$, which exists and is unique (Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (i), with $S=\mathbb{N}$ and $X$ in place of $Y$). Let $\mathrm{ev}:Y^{X}\times X\to Y$ be the evaluation map, the only map with $\mathrm{ev}(g,p)=g(p)$ for all $g\in Y^{X}$ and $p\in X$ (Projection, Evaluation and Currying Maps (ii), with $I=X$). By Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (iii), applied with $S=\mathbb{N}$, the maps $f:\mathbb{N}\to Y^{X}$ and $c:\mathbb{N}\to X$, and $F=\mathrm{ev}$, there is exactly one map $u:\mathbb{N}\to Y$ with $u(m)=\mathrm{ev}(f(m),c(m))$ for every $m\in\mathbb{N}$; this $u$ is the composite of $\mathrm{ev}$ with the map $m\mapsto(f_{m},x)$. For every $m\in\mathbb{N}$,

$$u(m)=\mathrm{ev}(f_{m},x)=f_{m}(x).$$

So $u$ is a sequence in $Y$ (Sequences (i)) with $u_{m}=f_{m}(x)$ for every $m\in\mathbb{N}$. If $v$ is any sequence in $Y$ with $v_{m}=f_{m}(x)$ for every $m\in\mathbb{N}$, then $v$ and $u$ are maps $\mathbb{N}\to Y$ with $v(m)=u(m)$ for every $m\in\mathbb{N}$, so $v=u$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv)). Hence $u$ is the only such sequence.

Proof of (ii). Since $u:\mathbb{N}\to Y$ is a map, its range is its image $u[\mathbb{N}]$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (v)). Let $y$ be a set. By The Image and the Preimage of a Class under a Class (i), $y\in u[\mathbb{N}]$ if and only if $(m,y)\in u$ for some $m\in\mathbb{N}$; and for $m\in\mathbb{N}$, $(m,y)\in u$ if and only if $y=u(m)$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i)), that is, $y=f_{m}(x)$ by (i). Hence $y\in\operatorname{ran}u$ if and only if $y=f_{m}(x)$ for some $m\in\mathbb{N}$. Every such $y$ lies in $Y$, as $u(m)\in Y$ for $m\in\mathbb{N}$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii)); so $\operatorname{ran}u\subseteq Y$, and $\operatorname{ran}u$ is a set (Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i)). It has exactly the elements of $\{f_{m}(x):m\in\mathbb{N}\}$, so by extensionality (Class Theory NBG: the Axioms, Standing Conventions and Basic Notation (ii)) it is the set $\{f_{m}(x):m\in\mathbb{N}\}$.