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

Preliminaries. $\mathbb{N}$ is a set by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii), and $[0,\infty]\subseteq[-\infty,\infty]$ are sets by The Extended Real Line, Its Order, and [0,∞] (ii). The order $\le$ of $[-\infty,\infty]$ is a total order by Order and Suprema in the Extended Real Line (i), hence a partial order by Partial and Total Orders on a Set and the Associated Strict Relation (ii), and $+$ is a binary operation on $[0,\infty]$ by Addition and Multiplication on [0,∞] (i). A set variable is fresh for finitely many given formulas, terms and variables if it is none of $x_{1},\dots,x_{k}$ and the given variables and occurs in none of the given formulas and terms; as many distinct fresh set variables as needed exist, since the set variables form an infinite list (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (i)). The class variables $E$, $L$, $Z$, $P$, $N$, $R$ and $Q$ are none of the set variables chosen below (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (i)). By the hypothesis of (i), each of $E$, $L$, $Z$, $P$, $N$, $R$ and $Q$ has the same value in every formula formed below, those of $\gamma$ and $a$ included, and they are distinct, as Iterated Operations Are Given by a Predicative Formula (i) and Predicative Formulas for Suprema and Infima, and Maps Defined by Suprema and Infima (i) require. Every formula formed below is built from predicative formulas by connectives and quantifiers over set variables, hence is predicative (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i)).

Let $c$ be a sequence in $[0,\infty]$ and $n\in\mathbb{N}$. Then $[n]=\{k\in\mathbb{N}:k\le n\}\subseteq\mathbb{N}$, so $c$ is a map from a set containing $[n]$ to $[0,\infty]$, and its $n$-th partial sum $\sum_{j=1}^{n}c_{j}$ of Sum of a Sequence in [0,∞] (i) lies in $[0,\infty]$, by that clause. By Sum of a Sequence in [0,∞] (ii), $\sum_{j\in\mathbb{N}}c_{j}=\sup\Pi(c)$, formed in $[-\infty,\infty]$ with $\le$, where $\Pi(c)=\{\sum_{j=1}^{n}c_{j}:n\in\mathbb{N}\}$ is the set of the partial sums, a subset of $[0,\infty]$; and $\sum_{j\in\mathbb{N}}c_{j}\in[0,\infty]$.

Proof of (i). Under an assignment satisfying $\gamma$, the value $c$ of $a$ is a set in $\mathcal{S}$ by Terms and Typed Terms under a Guard (iii), so $c$ is a sequence in $[0,\infty]$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i) and Sequences (i). Below, $c$ always denotes this value.

Values. Under an assignment satisfying $\gamma$, the value $\sum_{j\in\mathbb{N}}c_{j}$ of $\sum_{j\in\mathbb{N}}a_{j}$ is a set lying in $[0,\infty]$ by the preliminaries, determined by $c$, hence by the sets assigned to $x_{1},\dots,x_{k}$ and the values of the parameters. So $\sum_{j\in\mathbb{N}}a_{j}$ is a term under $\gamma$ satisfying Terms and Typed Terms under a Guard (iii) with $[0,\infty]$.

The formula. Let $z$ be a set variable that is none of $x_{1},\dots,x_{k}$, is not free in $\gamma$ and does not occur in $\sum_{j\in\mathbb{N}}a_{j}$, so that it occurs neither in $a$ nor among its parameters.

Step 1: the partial sums. Choose a set variable $n$ fresh for $\gamma$, $a$ and $z$. The formula $(\gamma\wedge n\in N)$ is predicative, with free variables among $x_{1},\dots,x_{k}$, $n$ and the parameters, so it is a guard $\gamma'$ for the variables $x_{1},\dots,x_{k},n$ (Conditions Expressed by a Predicative Formula, and Guards (iii)). Since $n$ is not free in $\gamma$ and does not occur in $a$, an assignment to $x_{1},\dots,x_{k},n$ satisfies $\gamma'$ if and only if its part on $x_{1},\dots,x_{k}$ satisfies $\gamma$ and the set assigned to $n$ lies in $\mathbb{N}$; then the value $c$ of $a$ is defined, and we let $s$ be the term under $\gamma'$, written with $a$, $n$, $Z$, $P$, $N$, $R$ and $Q$, whose value is $\sum_{j=1}^{n}c_{j}$. It lies in $[0,\infty]$ by the preliminaries and is determined by the assigned sets and the parameters, so $s$ is a term under $\gamma'$ satisfying Terms and Typed Terms under a Guard (iii) with $[0,\infty]$.

Let $y$ be a set variable that is none of $x_{1},\dots,x_{k}$ and $n$, is not free in $\gamma'$ and does not occur in $s$; and choose a set variable $v$ fresh for $\gamma$, $a$, $n$ and $y$. By Terms and Typed Terms under a Guard (iv) for $a$, a predicative formula $\psi_{v}$ expresses $\gamma\wedge v=a$ on $x_{1},\dots,x_{k}$ and $v$; by Conditions Expressed by a Predicative Formula, and Guards (ii), its free variables are among $x_{1},\dots,x_{k}$, $v$ and the parameters of $\gamma$ and $a$, so neither $n$ nor $y$ is free in it. By Iterated Operations Are Given by a Predicative Formula (i), applied to the distinct set variables $y$, $n$ and $v$ for its $w$, $n$ and $a$ and the class variables $Z$, $P$, $N$, $R$ and $Q$ for its $X$, $F$, $Y$, $R$ and $P$, there is a predicative formula $\mathrm{it}(y,n,v)$, with free variables among $y$, $n$, $v$, $Z$, $P$, $N$, $R$ and $Q$, such that for every $n\in\mathbb{N}$, every map $v$ from a set containing $[n]$ to $[0,\infty]$, and every set $y$, $\mathrm{it}(y,n,v)$ holds if and only if $y=\sum_{j=1}^{n}v_{j}$. Let $\chi_{y}$ be the formula $\exists v\,(\psi_{v}\wedge n\in N\wedge\mathrm{it}(y,n,v))$; it is predicative, with free variables among $x_{1},\dots,x_{k}$, $n$, $y$ and the parameters of $\gamma'$ and $s$. Under an assignment of sets to $x_{1},\dots,x_{k}$, $n$ and $y$, $\chi_{y}$ holds if and only if $\gamma$ holds, $n\in\mathbb{N}$ and $\mathrm{it}(y,n,c)$, since the only set $v$ with $\psi_{v}$ is then $c$; as $c$ is a map from $\mathbb{N}\supseteq[n]$ to $[0,\infty]$, this holds if and only if $\gamma'$ holds and $y=\sum_{j=1}^{n}c_{j}$. So $\chi_{y}$ expresses $\gamma'\wedge y=s$, Terms and Typed Terms under a Guard (iv) holds, and $s$ is a term of type $[0,\infty]$ under $\gamma'$ by Terms and Typed Terms under a Guard (ii).

Step 2: the set of partial sums. By Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term (iv), with $n$ for its $u$, $N$ for its $D$, $[0,\infty]$ for its $B$, $s$ for its $t$ and the power set $\mathcal{P}([0,\infty])$, whose elements are the subsets of $[0,\infty]$, for its $C$, the image $T=\{s:n\in N\}$ is a term of type $\mathcal{P}([0,\infty])$ under $\gamma$; its hypotheses hold, as $n$ is none of $x_{1},\dots,x_{k}$ and not free in $\gamma$, and $N$ is a variable other than $x_{1},\dots,x_{k}$ and $n$ whose value $\mathbb{N}$ is a set. By Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term (i), under each assignment satisfying $\gamma$ the value of $T$ has as elements exactly the sets $\sum_{j=1}^{n}c_{j}$, $n\in\mathbb{N}$, so it is $\Pi(c)$ by Axiom of Extensionality for Classes.

Step 3: the supremum. Choose distinct set variables $q$, $b$ and $w$ fresh for $\gamma$, $a$, $n$ and $z$. Then $q$ is none of $x_{1},\dots,x_{k}$, is not free in $\gamma$ and does not occur in $T$, bound occurrences counting, as $T$ is written with $s$, $n$ and $N$; so by Terms and Typed Terms under a Guard (iv) for $T$ a predicative formula $\psi_{T}$ expresses $\gamma\wedge q=T$ on $x_{1},\dots,x_{k}$ and $q$, and its free variables are among $x_{1},\dots,x_{k}$, $q$ and the parameters of $\gamma$ and $T$, so $z$ is not free in it. Let $\sigma(q,z)$ be the formula of Predicative Formulas for Suprema and Infima, and Maps Defined by Suprema and Infima (i) for the set $[-\infty,\infty]$, the value of $E$, with the partial order $\le$, the value of $L$, written with $E$ and $L$ for its $p$ and $\preceq$ and with the distinct set variables $q$, $z$, $b$ and $w$ for its $S$, $z$, $b$ and $v$. It is predicative, its free variables are among $q$, $z$, $E$ and $L$, and for sets $q$ and $z$ it holds if and only if $q$ is a subset of $[-\infty,\infty]$ that has a supremum and $z=\sup q$, suprema being those of Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order formed in $[-\infty,\infty]$ with $\le$. Let $\chi$ be the formula $\exists q\,(\psi_{T}\wedge\sigma(q,z))$. It is predicative, and its free variables are among $x_{1},\dots,x_{k}$, $z$ and the parameters of $\gamma$ and $\sum_{j\in\mathbb{N}}a_{j}$. Under an assignment of sets to $x_{1},\dots,x_{k}$ and $z$, $\chi$ holds if and only if $\gamma$ holds and $\sigma(\Pi(c),z)$, by Step 2. The set $\Pi(c)$ is a subset of $[0,\infty]\subseteq[-\infty,\infty]$, which has a supremum by Order and Suprema in the Extended Real Line (iii); so $\chi$ holds if and only if $\gamma$ holds and $z=\sup\Pi(c)=\sum_{j\in\mathbb{N}}c_{j}$, by the preliminaries. So $\chi$ expresses $\gamma\wedge z=\sum_{j\in\mathbb{N}}a_{j}$, which is Terms and Typed Terms under a Guard (iv), and $\sum_{j\in\mathbb{N}}a_{j}$ is a term of type $[0,\infty]$ under $\gamma$ by Terms and Typed Terms under a Guard (ii).

Proof of (ii). Let $D'$ and $F$ be class variables, distinct from $E$, $L$, $Z$, $P$, $N$, $R$ and $Q$, whose values are $D$ and the map $i\mapsto a^{(i)}$, and let $i$ be a set variable. With $k=1$ and $i$ for $x_{1}$, the formula $i\in D'$ is a guard $\gamma_{D}$, and an assignment satisfies it exactly when the set assigned to $i$ lies in $D$. By Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (i), $i$ is a term of type $D$ under $\gamma_{D}$, and by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), $F(i)$ is a term of type $\mathcal{S}$ under $\gamma_{D}$, with value $a^{(i)}$. By (i), $\sum_{j\in\mathbb{N}}F(i)_{j}$ is a term of type $[0,\infty]$ under $\gamma_{D}$, whose value at $i\in D$ is $\sum_{j\in\mathbb{N}}a^{(i)}_{j}$. Let $z$ be a set variable other than $i$ that does not occur in this term. By Terms and Typed Terms under a Guard (iv), a predicative formula $\theta(z,i)$, with free variables among $z$, $i$ and the class variables named above, expresses $\gamma_{D}\wedge z=\sum_{j\in\mathbb{N}}F(i)_{j}$. So for every $i\in D$ exactly one set $z$ satisfies $\theta(z,i)$, namely $\sum_{j\in\mathbb{N}}a^{(i)}_{j}$, which lies in $[0,\infty]$ by Terms and Typed Terms under a Guard (iii). By Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (viii), $\sum_{j\in\mathbb{N}}a^{(i)}_{j}$ is therefore a defined set symbol with argument $i$, given by $\theta$ and used properly at every $i\in D$. As $D$ and $[0,\infty]$ are sets, Maps and Relations Given by Formulas (i), applied to $D$, $[0,\infty]$ and this expression, gives exactly one map $f:D\to[0,\infty]$ with $f(i)=\sum_{j\in\mathbb{N}}a^{(i)}_{j}$ for every $i\in D$.