Sums of Sequences in [0,∞] as Typed Terms and as a Map

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $[-\infty,\infty]$, $[0,\infty]$ and the order $\le$ of $[-\infty,\infty]$ be as in The Extended Real Line, Its Order, and [0,∞] (ii) and The Extended Real Line, Its Order, and [0,∞] (iii), the sum $+$ on $[0,\infty]$ as in Addition and Multiplication on [0,∞] (i), and the sum $\sum_{j\in\mathbb{N}}c_{j}$ of a sequence $(c_{j})$ in $[0,\infty]$ as in Sum of a Sequence in [0,∞] (ii). Let $\mathcal{S}=[0,\infty]^{\mathbb{N}}$ be the class of functions from $\mathbb{N}$ to $[0,\infty]$; by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i) its elements are exactly the maps $\mathbb{N}\to[0,\infty]$, that is, the sequences in $[0,\infty]$, and it is a set by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (ii). (i) is a statement of the metatheory about expressions.

(i) Let $k\ge0$, the distinct set variables $x_{1},\dots,x_{k}$, the parameters with their fixed values, and assignments be as in Conditions Expressed by a Predicative Formula, and Guards (i); let $\gamma$ be a guard; and let terms under $\gamma$ and their values, and terms of type $A$ under $\gamma$ for a class $A$, be as in Terms and Typed Terms under a Guard (i) and Terms and Typed Terms under a Guard (ii). Let $E$, $L$, $Z$, $P$, $N$, $R$ and $Q$ be distinct class variables whose values are $[-\infty,\infty]$, its order $\le$, $[0,\infty]$, the sum $+$ on $[0,\infty]$, $\mathbb{N}$, and the order and the addition of $\mathbb{N}_{0}$, and none of which is a parameter of $\gamma$ or of $a$ with a different value. Let $a$ be a term of type $\mathcal{S}$ under $\gamma$, and let $\sum_{j\in\mathbb{N}}a_{j}$ be the term under $\gamma$, written with $a$ and the parameters $E$, $L$, $Z$, $P$, $N$, $R$ and $Q$, whose value under each assignment satisfying $\gamma$ is the sum of the sequence in $[0,\infty]$ that is the value of $a$. Then $\sum_{j\in\mathbb{N}}a_{j}$ is a term of type $[0,\infty]$ under $\gamma$.

(ii) Let $D$ be a set and let $i\mapsto a^{(i)}$ be a map from $D$ to $\mathcal{S}$, so that each $a^{(i)}$ is a sequence in $[0,\infty]$, with terms $a^{(i)}_{j}$. Then there is exactly one map $f:D\to[0,\infty]$ with $f(i)=\sum_{j\in\mathbb{N}}a^{(i)}_{j}$ for every $i\in D$.