The Sequences k ↦ $f_k(p)$ of a Sequence in ℝ^I, and the Map of Their Limits

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $I$ be a set, let $\mathbb{R}^{I}$ be the set of maps from $I$ to $\mathbb{R}$ of Sets and Maps: Ordinary Notation §maps, let $d_{\mathbb{R}}$ be the distance on $\mathbb{R}$ of Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces §real-line, and let $(f_{k})_{k\in\mathbb{N}}$ be a sequence in $\mathbb{R}^{I}$.

¶ For every $p\in I$, the map $k\mapsto f_{k}(p)$ on $\mathbb{N}$, written $(f_{k}(p))_{k}$, is a sequence in $\mathbb{R}$, with $k$-th term $f_{k}(p)$.

¶ If for every $p\in I$ the sequence $(f_{k}(p))_{k}$ is convergent in $(\mathbb{R},d_{\mathbb{R}})$, then there is exactly one $L\in\mathbb{R}^{I}$ such that, for every $p\in I$, $(f_{k}(p))_{k}$ converges to $L(p)$ in $(\mathbb{R},d_{\mathbb{R}})$; and $L(p)$ is the limit $\lim_{k\to\infty}f_{k}(p)$ in $(\mathbb{R},d_{\mathbb{R}})$ for every $p\in I$.

¶ If for every $p\in I$ the sequence $(f_{k}(p))_{k}$ is convergent in the sense of Convergent Sequences of Real Numbers §converges, then there is exactly one $L\in\mathbb{R}^{I}$ such that, for every $p\in I$, $(f_{k}(p))_{k}$ converges to $L(p)$ in that sense; this $L$ is the map of the clause limit-map, and $L(p)$ is the limit $\lim_{k\to\infty}f_{k}(p)$ of The Limit of a Convergent Sequence §limit for every $p\in I$.