Kit for def:iterated-operation-nbg

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $n\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{n-1}$ be distinct set variables, and let $i,j,k,l,m<n$, not necessarily distinct. Segments $[x]$ are as in Intervals of Natural Numbers (ii).

(i) The recursion of an iterated operation. The condition "$x_{j}$ is a binary operation on $x_{i}$, $x_{k}\in\mathbb{N}$, $x_{l}$ and $x_{m}$ are maps $[x_{k}]\to x_{i}$, $x_{m}(1)=x_{l}(1)$, and $x_{m}(r+1)=x_{m}(r)\ast x_{l}(r+1)$ for every $r\in[x_{k}]$ with $r<x_{k}$, where $\ast$ is the operation $x_{j}$" on $x_{0},\dots,x_{n-1}$ is predicative: expressed by a predicative formula, with $x_{0},\dots,x_{n-1}$ in place of the variables of Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables; $\mathbb{N}$, the order $\le$ of $\mathbb{N}_{0}$ and the addition $+$ of $\mathbb{N}_{0}$ are parameters.