Proof of Partial Sums of a Sequence of Functions into [0,∞]

Write $P=[0,\infty]^{X}$, a set whose elements are exactly the functions $X\to[0,\infty]$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (ii), The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)), and let $[n]$, for $n\in\mathbb{N}$, be the segment $\{1,\dots,n\}$, a subset of $\mathbb{N}$ (Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i)).

The pointwise sum and evaluation. For $g,h\in P$, the sum $g+h$ of Sums, Multiples and Products of Functions into [0,∞] (i) lies in $P$, so there is a function $\oplus:P\times P\to P$ with $g\oplus h=g+h$ for all $g,h\in P$ (Maps and Relations Given by Formulas (ii)); it is a binary operation on $P$. For $x\in X$, the function $\varepsilon_{x}:P\to[0,\infty]$, $g\mapsto g(x)$, exists by Maps and Relations Given by Formulas (i), and by Sums, Multiples and Products of Functions into [0,∞] (i)

$$\varepsilon_{x}(g\oplus h)=(g+h)(x)=g(x)+h(x)=\varepsilon_{x}(g)+\varepsilon_{x}(h)\qquad(g,h\in P).$$

The partial-sum functions. As $(f_{k})$ is a sequence in $P$, Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (i) gives a function $H:\mathbb{N}\to P$ with

$$H(n)=\mathop{\oplus}\limits_{k=1}^{n}f_{k}\qquad(n\in\mathbb{N}),$$

the iterated operation of $\oplus$ being read as in Iterated Operations: Finite Sums and Finite Products (ii). Thus $H$ is a sequence $(H_{n})$, $H_{n}=H(n)$, of functions $X\to[0,\infty]$.

Their values. Let $n\in\mathbb{N}$, $x\in X$, and let $u$ be a sequence in $[0,\infty]$ with $u_{k}=f_{k}(x)$ for every $k\in\mathbb{N}$. Let $a:[n]\to P$ and $b:[n]\to[0,\infty]$ be the restrictions of $(f_{k})$ and of $u$ to $[n]$, so that $a_{k}=f_{k}$ and $b_{k}=u_{k}$ for $k\in[n]$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ix)). By the display above and Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms (ii), applied to $\varepsilon_{x}$,

$$H_{n}(x)=\varepsilon_{x}\Bigl(\mathop{\oplus}\limits_{k=1}^{n}a_{k}\Bigr)=\sum_{k=1}^{n}\varepsilon_{x}(a_{k}).$$

The function $[n]\to[0,\infty]$, $k\mapsto\varepsilon_{x}(a_{k})=f_{k}(x)=u_{k}$, has the domain and values of $b$, so it is $b$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i)). Hence

$$H_{n}(x)=\sum_{k=1}^{n}b_{k}=\sum_{k=1}^{n}u_{k},$$

the $n$-th partial sum of $u$ (Iterated Operations: Finite Sums and Finite Products (ii), Sum of a Sequence in [0,∞] (i)). This is (i).