Proof of Iterated Operations and Operations over Finite Sets Take Values in the Underlying Set

Each result cited is universally quantified over the data in its own statement. No choice is used.

Value rule. If $g:B\to C$ is a map and $u\in B$, then $g(u)\in C$: indeed $u\in B=\operatorname{dom}g$ by Functions, Values of a Function, and Functions from One Class to Another §map, so $(u,g(u))\in g$ by Functions, Values of a Function, and Functions from One Class to Another §value, whence $g(u)\in\operatorname{ran}g$ by Relations, Domain, Range, Inverse and Composition §range and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, and $\operatorname{ran}g\subseteq C$ by Functions, Values of a Function, and Functions from One Class to Another §map.

Clause iterated. Let $n\in\mathbb{N}$ and $a:[n]\to X$. By Iterated Operations: Finite Sums and Finite Products §iterated, $\mathop{\ast}\limits_{k=1}^{n}a_{k}=s(n)$, where $s:[n]\to X$ is the map of Iterating a Binary Operation along a Finite List §existence for $\ast$ and $a$, unique by that clause, and $n\in[n]$, as in Iterated Operations: Finite Sums and Finite Products §iterated. Hence $\mathop{\ast}\limits_{k=1}^{n}a_{k}=s(n)\in X$ by the value rule.

Clause finite. Let $\ast$ be associative and commutative, let $A$ be a finite set and $f:A\to X$ a map, and let $A\neq\emptyset$ or let $\ast$ have a neutral element $e$.

If $A=\emptyset$, then $\ast$ has a neutral element $e$ by hypothesis, $\mathop{\ast}\limits_{x\in A}f(x)=e$ by Sums and Products over a Finite Set and over an Interval §empty, and $e\in X$ by Associative and Commutative Binary Operations, and Neutral Elements §neutral.

If $A\neq\emptyset$, let $n=\#A$ be as in The Number of Elements of a Finite Set §cardinality; then $n\in\mathbb{N}$ by The Iterated Operation over a Finite Set Does Not Depend on the Enumeration §nonempty, and by The Number of Elements of a Finite Set §cardinality there is a bijection $\varphi$ from $[n]$ onto $A$; fix one. By Injective, Surjective and Bijective Functions between Classes §bijective, $\varphi$ is a map $\varphi:[n]\to A$. As $f:A\to X$ is a map, Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition shows that the composition $f\circ\varphi$ is a map $f\circ\varphi:[n]\to X$ with $(f\circ\varphi)(k)=f(\varphi(k))$ for every $k\in[n]$; in particular $f(\varphi(k))\in X$ for every $k\in[n]$, by the value rule. The map $k\mapsto f(\varphi(k))$ on $[n]$ of Iterated Operations: Finite Sums and Finite Products §iterated is a function with domain $[n]$ and value $f(\varphi(k))$ at every $k\in[n]$, and so is $f\circ\varphi$, by Functions, Values of a Function, and Functions from One Class to Another §map; hence the two are equal by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality. Let $a=f\circ\varphi$, with $a_{k}=a(k)$ for $k\in[n]$. By Sums and Products over a Finite Set and over an Interval §operation and Iterated Operations: Finite Sums and Finite Products §iterated,

$$\mathop{\ast}\limits_{x\in A}f(x)=\mathop{\ast}\limits_{k=1}^{n}f(\varphi(k))=\mathop{\ast}\limits_{k=1}^{n}a_{k},$$

which lies in $X$ by the clause iterated, applied to $n$ and $a$.

Clauses finite-sums and segment-sums. Let $A$ be a finite set, $f:A\to R$ a map, $n\in\mathbb{N}$ and $a:[n]\to R$ a map. By the framing of Commutative Rings §ring, $R$ is a set and $+$ and $\cdot$ are binary operations on $R$, and by Commutative Rings, Fields and Ordered Fields: Standard Notation §rings they are associative and commutative with neutral elements $0$ and $1$. By Commutative Rings, Fields and Ordered Fields: Standard Notation §rings, $\sum_{x\in A}f(x)$ and $\prod_{x\in A}f(x)$ are the iterated operations over $A$ of Sums and Products over a Finite Set and over an Interval §operation and Sums and Products over a Finite Set and over an Interval §empty for $\ast$ equal to $+$ and to $\cdot$, respectively, where by Sums and Products over a Finite Set and over an Interval §subsets, as $+$ and $\cdot$ have neutral elements, the iterated operation over $A$ of $f$ is that of the restriction $f|_{A}$. Here $f|_{A}=f$: by Functions, Values of a Function, and Functions from One Class to Another §map, $f$ is a function with $\operatorname{dom}f=A$, so by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction $f|_{A}$ is a function with $\operatorname{dom}(f|_{A})=A\cap A=A$ and $(f|_{A})(u)=f(u)$ for every $u\in A$, and $f|_{A}=f$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality. So $\sum_{x\in A}f(x)$ and $\prod_{x\in A}f(x)$ are the iterated operations over $A$ of the map $f:A\to R$ itself. By Iterated Operations: Finite Sums and Finite Products §sums, $\sum_{k=1}^{n}a_{k}$ and $\prod_{k=1}^{n}a_{k}$ are the iterated operations along $[n]$ for $\ast$ equal to $+$ and to $\cdot$, respectively. Hence the clause finite, applied with $X=R$, once with $\ast=+$ and $e=0$ and once with $\ast=\cdot$ and $e=1$, gives $\sum_{x\in A}f(x)\in R$ and $\prod_{x\in A}f(x)\in R$, which is the clause finite-sums; and the clause iterated, applied with $X=R$, once with $\ast=+$ and once with $\ast=\cdot$, gives $\sum_{k=1}^{n}a_{k}\in R$ and $\prod_{k=1}^{n}a_{k}\in R$, which is the clause segment-sums.