The Set of Indices n for Which the n-th Map of a Sequence in ℝ^[a,b] Is Integrable with a Prescribed Integral

In the setting of The Real Line: Standing Notation and Background for Calculus on Intervals, with predicative meant for formulas with abbreviations, conditions expressed by a predicative formula are as in Conditions Expressed by a Predicative Formula, and Guards (ii), with parameters and their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i). Let $a,b\in\mathbb{R}$ with $a<b$, let $(h_{n})_{n\in\mathbb{N}}$ be a sequence in the set $\mathbb{R}^{[a,b]}$ of maps from $[a,b]$ to $\mathbb{R}$ of Sets and Maps: Ordinary Notation (v), and let $(z_{n})_{n\in\mathbb{N}}$ be a sequence in $\mathbb{R}$. A map $h:[a,b]\to\mathbb{R}$ is bounded if there is $B\in\mathbb{R}$ with $|h(t)|\le B$ for every $t\in[a,b]$; for a bounded such $h$, integrability on $[a,b]$ and the integral $\int_{a}^{b}h$ are as in The Riemann Integral on a Closed Interval via Lower and Upper Integrals (iv) and The Riemann Integral on a Closed Interval via Lower and Upper Integrals (v).

(i) The condition "$n\in\mathbb{N}$, $h_{n}$ is bounded and integrable on $[a,b]$ and $\int_{a}^{b}h_{n}=z_{n}$" on the set variable $n$, with parameters $a$, $b$, $[a,b]$, the maps $(h_{n})_{n\in\mathbb{N}}$ and $(z_{n})_{n\in\mathbb{N}}$, and the parameters other than $E$ listed in A Predicative Formula for the Oriented Riemann Integral, and Maps Given by Integrals (i), is expressed by a predicative formula; this is a statement of the metatheory. The class

$$A=\{n\in\mathbb{N}:h_{n}\text{ is bounded and integrable on }[a,b]\text{ and }\textstyle\int_{a}^{b}h_{n}=z_{n}\},$$

formed as in Sets and Maps: Ordinary Notation (iii) from a predicative formula expressing this condition, is a set and a subset of $\mathbb{N}$, and it does not depend on the choice of that formula. For every set $m$: $m\in A$ if and only if $m\in\mathbb{N}$, $h_{m}$ is bounded and integrable on $[a,b]$ and $\int_{a}^{b}h_{m}=z_{m}$.