A Finite Sum of Nonnegative Real Numbers in [0,∞] Is Their Real Sum

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $\infty$ and $[0,\infty]$ be as in The Extended Real Line, Its Order, and [0,∞] (i) and The Extended Real Line, Its Order, and [0,∞] (ii). Sums over a finite set are as in Sums and Products over a Finite Set and over an Interval (i), Sums and Products over a Finite Set and over an Interval (ii), Sums and Products over a Finite Set and over an Interval (iii) and Sums and Products over a Finite Set and over an Interval (v). For a finite set $I$ and a function $v$ from a set containing $I$ to $\mathbb{R}$, $\sigma_{\mathbb{R}}(v,I)=\sum_{i\in I}v(i)$ is its sum over $I$ for the sum on $\mathbb{R}$; for such a function $v$ into $[0,\infty]$, $\sigma_{[0,\infty]}(v,I)=\sum_{i\in I}v(i)$ is its sum over $I$ for the sum $+$ on $[0,\infty]$ of Addition and Multiplication on [0,∞] (i). Like the sum on $\mathbb{R}$, this sum is associative and commutative with neutral element $0$ (Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i)).

(i) The two sums agree. Let $I$ be a finite set and let $u:I\to\mathbb{R}$ be a function with $0\le u(i)$ for every $i\in I$. Then $u$ is also a function $u:I\to[0,\infty]$, and

$$\sigma_{[0,\infty]}(u,I)=\sigma_{\mathbb{R}}(u,I);$$

in particular $\sigma_{[0,\infty]}(u,I)$ is a real number.