Kit for def:lebesgue-integral-nonnegative

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity and Measurable Functions and the Lebesgue Integral: Notation, let $(X,\mathcal{F})$ be a measurable space. Let $N\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{N-1}$ be distinct set variables, and let $i,j<N$, not necessarily distinct. The parameters, each other than $x_{0},\dots,x_{N-1}$, are the distinct set variables $X$, $\mathcal{F}$, $\mathcal{S}^{+}$ and $\mathcal{M}^{+}$, with values $X$, $\mathcal{F}$, $\mathcal{S}^{+}(X,\mathcal{F})$ and $\mathcal{M}^{+}(X,\mathcal{F})$; the ten parameters $E$, $L$, $Z$, $P$, $\mathbb{N}$, $R$, $Q$, $\infty$, $0$ and $1$ of Kit for def:measure-measure-space, with the kinds and values given there; and the parameters of The Simple, Nonnegative, Integrable and Signed Integrals Are Predicative in the Measure and the Function, at Any Variable Positions (ii) for $(X,\mathcal{F})$, of which its $X$, $\mathcal{F}$, $\mathcal{S}^{+}$ and $\mathcal{M}^{+}$ are the variables of these names, those whose values are the values of $E$, $L$, $Z$, $P$, $\mathbb{N}$, $R$, $Q$, $\infty$, $0$ and $1$ are those variables, and the others are further distinct class variables, other than all the above, with their values there. A condition on $x_{0},\dots,x_{N-1}$ is predicative if it is 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), no displayed variables, and these parameters.

(i) The integral as a map. With $\mu=x_{i}$ and $J=x_{j}$, the condition "$\mu$ is a measure on $(X,\mathcal{F})$ and $J$ is the integral with respect to $\mu$, the map $\mathcal{M}^{+}\to[0,\infty]$, $f\mapsto\int f\,d\mu$" is predicative.