Iterated Operations over Finite Sets Are Given by a Predicative Formula

In the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, let finite sets be as in Finite Sets §finite, and let iterated operations over finite sets be as in Sums and Products over a Finite Set and over an Interval §operation, Sums and Products over a Finite Set and over an Interval §empty and Sums and Products over a Finite Set and over an Interval §subsets. The clause below is a statement of the metatheory. Formulas may be written with abbreviations, defined set symbols being used properly, and predicative is meant as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols; set variables, class variables and free variables are as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols, and sets and classes are assigned to them as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading.

¶ Let $w$, $C$ and $g$ be any distinct set variables and $X$, $F$, $Y$, $R$ and $P$ any distinct class variables. There is a predicative formula $\mathrm{fop}(w,C,g)$, whose free variables are among $w$, $C$, $g$, $X$, $F$, $Y$, $R$ and $P$, with the following property. Let a set, an associative and commutative binary operation $\ast$ on it that has a neutral element, $\mathbb{N}$ (as in The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets), the order $\le$ of $\mathbb{N}_{0}$ and the addition $+$ of $\mathbb{N}_{0}$ be assigned to $X$, $F$, $Y$, $R$ and $P$, respectively, and write $X$ also for the set assigned to $X$. Then for every finite set $C$, every map $g$ from a set containing $C$ to $X$, and every set $w$, $\mathrm{fop}(w,C,g)$ holds if and only if $w=\mathop{\ast}\limits_{x\in C}g(x)$.