Sum of a Sequence in [0,∞]

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $[0,\infty]$ be as in The Extended Real Line, Its Order, and [0,∞] (ii), its sum $+$ as in Addition and Multiplication on [0,∞] (i), and suprema in $[-\infty,\infty]$, for its order of The Extended Real Line, Its Order, and [0,∞] (iii), as in Order and Suprema in the Extended Real Line (iii). Let $(a_{k})$ be a sequence in $[0,\infty]$.

(i) For $n\in\mathbb{N}$, the $n$-th partial sum of $(a_{k})$ is the iterated operation $s_{n}=\sum_{k=1}^{n}a_{k}$ of $+$ on $[0,\infty]$, as in Iterated Operations: Finite Sums and Finite Products (ii) and Iterated Operations: Finite Sums and Finite Products (iii). As $+$ is a binary operation on $[0,\infty]$, $(s_{n})$ is a sequence in $[0,\infty]$, the map $n\mapsto s_{n}$ on $\mathbb{N}$ existing by Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (i).

(ii) The sum of $(a_{k})$ is

$$\sum_{k\in\mathbb{N}}a_{k}=\sup\{s_{n}:n\in\mathbb{N}\},$$

which exists by Order and Suprema in the Extended Real Line (iii) and lies in $[0,\infty]$ by Order and Suprema in the Extended Real Line (ix), the set of the partial sums being a nonempty subset of $[0,\infty]$. For an expression $t(k)$ with $t(k)\in[0,\infty]$ for every $k\in\mathbb{N}$, $\sum_{k\in\mathbb{N}}t(k)$ is the sum of the sequence $k\mapsto t(k)$.