Iterated Operations 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 iterated operations be as in Iterated Operations: Finite Sums and Finite Products §iterated and Iterated Operations: Finite Sums and Finite Products §restriction, and $[n]$ as in Intervals of Natural Numbers §segment. 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$, $n$ and $a$ be any distinct set variables and $X$, $F$, $Y$, $R$ and $P$ any distinct class variables. There is a predicative formula $\mathrm{it}(w,n,a)$, whose free variables are among $w$, $n$, $a$, $X$, $F$, $Y$, $R$ and $P$, with the following property. Let a set, a binary operation $\ast$ on it, $\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 $n\in\mathbb{N}$, every map $a$ from a set containing $[n]$ to $X$, and every set $w$, $\mathrm{it}(w,n,a)$ holds if and only if $w=\mathop{\ast}\limits_{k=1}^{n}a_{k}$.