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

Each result cited is universally quantified over the data in its own statement.

Clause sections. Let $p\in I$. For $k\in\mathbb{N}$, $f_{k}\in\mathbb{R}^{I}$, so $f_{k}(p)\in\mathbb{R}$. So $k\mapsto f_{k}(p)$ is a map $s_{p}:\mathbb{N}\to\mathbb{R}$ with $s_{p}(k)=f_{k}(p)$ for every $k\in\mathbb{N}$, that is, a sequence in $\mathbb{R}$ with $k$-th term $f_{k}(p)$, by Sequences §sequence.

The sequence $s_{p}$ as an expression in $p$. For $p\in I$, $s_{p}$ is the only set satisfying a predicative formula $\theta(h,p)$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §map-symbol, with $\mathbb{N}$ and $\mathbb{R}$ for its $A$ and $B$, $p$ for its $v_{1}$, the guard $p\in I$, and the expression $f(k)(p)$ in $k$ and $p$, with $f$, $I$, $\mathbb{N}$ and $\mathbb{R}$ as parameters). So $s_{p}$ is a defined set symbol in $p$, used properly for $p\in I$, and an expression in $p$ of the kind Predicative Formulas for Convergence and Limits, and Maps Defined by Limits §maps takes.

Clause limit-map. By hypothesis, $s_{p}$ is convergent in the metric space $(\mathbb{R},d_{\mathbb{R}})$ for every $p\in I$. So there is a map $L:I\to\mathbb{R}$ with $L(p)=\lim s_{p}$ for every $p\in I$ (Predicative Formulas for Convergence and Limits, and Maps Defined by Limits §maps, with $(\mathbb{R},d_{\mathbb{R}})$ for its $(X,d)$, $I$ for its $a$ and $s_{p}$ for its $t(u)$), where $\lim s_{p}$ is the limit $\lim_{k\to\infty}f_{k}(p)$ of $s_{p}$ in $(\mathbb{R},d_{\mathbb{R}})$ of The Limit of a Convergent Sequence in a Metric Space §limit (Predicative Formulas for Convergence and Limits, and Maps Defined by Limits §limit-symbol). Then $L\in\mathbb{R}^{I}$, and for every $p\in I$, $s_{p}$ converges to $L(p)$ in $(\mathbb{R},d_{\mathbb{R}})$ by The Limit of a Convergent Sequence in a Metric Space §converges-to-limit. This proves existence and the description of $L(p)$.

For uniqueness, let $L'\in\mathbb{R}^{I}$ be such that $s_{p}$ converges to $L'(p)$ in $(\mathbb{R},d_{\mathbb{R}})$ for every $p\in I$. For $p\in I$, $s_{p}$ converges to both $L(p)$ and $L'(p)$, so $L'(p)=L(p)$ (Uniqueness of Limits in a Metric Space §unique). Hence $L'=L$.

Clause limit-map-real. By Convergence, Limits and the Cauchy Condition for Real Sequences Agree with Those in the Real Line as a Metric Space, which is Complete §converges, a sequence in $\mathbb{R}$ converges to $z\in\mathbb{R}$ in the sense of Convergent Sequences of Real Numbers §converges if and only if it converges to $z$ in $(\mathbb{R},d_{\mathbb{R}})$. Let every $s_{p}$ be convergent in the first sense. Then every $s_{p}$ is convergent in $(\mathbb{R},d_{\mathbb{R}})$ by Convergent Sequence in a Metric Space §convergent, and the clause limit-map gives its map $L\in\mathbb{R}^{I}$; for every $p\in I$, $s_{p}$ converges to $L(p)$ in $(\mathbb{R},d_{\mathbb{R}})$, hence in the first sense. If $L'\in\mathbb{R}^{I}$ is such that $s_{p}$ converges to $L'(p)$ in the first sense for every $p\in I$, then it does so in $(\mathbb{R},d_{\mathbb{R}})$, and $L'=L$ by the uniqueness in the clause limit-map. Finally, for $p\in I$, the limit $L(p)$ of $s_{p}$ in $(\mathbb{R},d_{\mathbb{R}})$ is its limit $\lim_{k\to\infty}f_{k}(p)$ of The Limit of a Convergent Sequence §limit (Convergence, Limits and the Cauchy Condition for Real Sequences Agree with Those in the Real Line as a Metric Space, which is Complete §limit).