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

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, maps and their values are as in Sets and Maps: Ordinary Notation (v). Let $X$ and $Y$ be sets and let $Y^{X}$ be the class of maps from $X$ to $Y$, which is a set (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (ii)) whose elements are exactly the maps $X\to Y$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)). Let $(f_{m})$ be a sequence in $Y^{X}$, so that each term $f_{m}$, for $m\in\mathbb{N}$, is a map $f_{m}:X\to Y$, and let $x\in X$.

(i) There is exactly one sequence $u$ in $Y$ with $u_{m}=f_{m}(x)$ for every $m\in\mathbb{N}$; it is written $(f_{m}(x))_{m}$.

(ii) The range of this sequence $u$ is the set $\{f_{m}(x):m\in\mathbb{N}\}$: for every set $y$, $y\in\operatorname{ran}u$ if and only if $y=f_{m}(x)$ for some $m\in\mathbb{N}$; and $\operatorname{ran}u\subseteq Y$.