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

For $i\in I$, $u(i)\in\mathbb{R}$ and $0\le u(i)$, so $u(i)\in[0,\infty]$ by The Extended Real Line, Its Order, and [0,∞] (ii). Hence the range of $u$ is contained in $[0,\infty]$, and $u:I\to[0,\infty]$ by Functions, Values of a Function, and Functions from One Class to Another (iii). So, for every finite set $C\subseteq I$, both $\sigma_{\mathbb{R}}(u,C)$ and $\sigma_{[0,\infty]}(u,C)$ are defined, and they lie in $\mathbb{R}$ and in $[0,\infty]$ respectively.

Let $\varphi(C)$ be the formula: if $C\subseteq I$, then $\sigma_{[0,\infty]}(u,C)=\sigma_{\mathbb{R}}(u,C)$. It is predicative, with parameters $I$, $u$ and the two sums (Iterated Operations over Finite Sets Are Given by a Predicative Formula (i)). We show $\varphi(C)$ for every finite set $C$ by Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (iii).

The empty set. By Sums and Products over a Finite Set and over an Interval (ii) and Sums and Products over a Finite Set and over an Interval (iii), the sum over $\emptyset$ is the neutral element of the operation, which is $0$ for the sum on $\mathbb{R}$ and $0$ for the sum on $[0,\infty]$, by Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i). So $\sigma_{[0,\infty]}(u,\emptyset)=0=\sigma_{\mathbb{R}}(u,\emptyset)$.

Adding a point. Let $C$ be a finite set with $\varphi(C)$, let $x\notin C$, and let $C\cup\{x\}\subseteq I$. Then $C\subseteq I$, so $s=\sigma_{[0,\infty]}(u,C)=\sigma_{\mathbb{R}}(u,C)$ is a real number. The set $\{x\}$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (iii), and $C\cup\{x\}$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (v). Let $f=u|_{C\cup\{x\}}$; its restrictions to $C$ and to $\{x\}$ are $u|_{C}$ and $u|_{\{x\}}$, and $C\cap\{x\}=\emptyset$. For each of the two sums, Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (ii) and Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (i), applied to $f$, give that the sum of $u$ over $C\cup\{x\}$ is the sum of $u$ over $C$ plus $u(x)$. Hence $\sigma_{[0,\infty]}(u,C\cup\{x\})$ is $s+u(x)$ formed in $[0,\infty]$; as $s$ and $u(x)$ are real, this is their sum in $\mathbb{R}$, by Addition and Multiplication on [0,∞] (i), which is $\sigma_{\mathbb{R}}(u,C\cup\{x\})$. So $\varphi(C\cup\{x\})$ holds.

Hence $\varphi(I)$ holds, as $I$ is finite; since $I\subseteq I$, $\sigma_{[0,\infty]}(u,I)=\sigma_{\mathbb{R}}(u,I)$, which is a real number.