Kit for def:riemann-integral

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity and The Real Line: Standing Notation and Background for Calculus on Intervals; this item is a statement of the metatheory. Let $N\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{N-1}$ be distinct set variables, and let $i,j,k,l<N$, not necessarily distinct. Each clause below states that a condition 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. The other letters, among them $\mathbb{R}$, its operations $+$ and $\cdot$, its elements $0$ and $1$, its order $\le$ and the strict order $<$ of $\le$, and $\mathbb{N}$, $\mathbb{N}_{0}$ and the order $\le$, the addition $+$ and the element $1$ of $\mathbb{N}_{0}$, are parameters. Such a formula, for instance one whose reading is the reading of a formula tree as in The Graph Reading of a Formula Tree Is Predicative and Agrees with Its Reading, So the Reading Is Predicative (iii), is what class comprehension (The Class Comprehension Theorem for Predicative Formulas (i)) and induction (Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1 (i)) apply to. None of the three notions below is a condition on a single set, so the kit has no clause on a class of sets satisfying one.

(i) Integrable functions. With $a=x_{i}$, $b=x_{j}$ and $f=x_{k}$, the condition "$a,b\in\mathbb{R}$, $a<b$, $f$ is a map $f:[a,b]\to\mathbb{R}$, bounded (there is $B\in\mathbb{R}$ with $|f(t)|\le B$ for every $t\in[a,b]$), and $f$ is Riemann integrable on $[a,b]$" is predicative.

(ii) Integrability on a subinterval. With $E=x_{i}$, $g=x_{j}$, $u=x_{k}$ and $v=x_{l}$, the condition "$E\subseteq\mathbb{R}$, $g$ is a map $g:E\to\mathbb{R}$, $u,v\in\mathbb{R}$, $u<v$, $[u,v]\subseteq E$, and $g$ is integrable on $[u,v]$" is predicative.

(iii) Defined integrals. With $E=x_{i}$, $g=x_{j}$, $u=x_{k}$ and $v=x_{l}$, the condition "$E\subseteq\mathbb{R}$, $g$ is a map $g:E\to\mathbb{R}$, $u,v\in E$, and $\int_{u}^{v}g$ is defined" is predicative.