A Predicative Formula for the Oriented Riemann Integral, and Maps Given by Integrals

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); (i) is a statement of the metatheory. For a subset $E$ of $\mathbb{R}$, a map $g:E\to\mathbb{R}$ and $u,v\in\mathbb{R}$ with $u<v$ and $[u,v]\subseteq E$, integrability of $g$ on $[u,v]$ and the integral $\int_{u}^{v}g$ are as in The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vi), and the oriented integrals $\int_{u}^{u}g$ and $\int_{v}^{u}g$ as in The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vii); for $u,v\in E$, whether $\int_{u}^{v}g$ is defined is as in The Riemann Integral on a Closed Interval via Lower and Upper Integrals (viii).

(i) Let $E$ be a subset of $\mathbb{R}$. The letters $g$, $u$, $v$ and $z$ are distinct set variables, and $E$, $\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. Then the condition "$g$ is a map $g:E\to\mathbb{R}$, $u,v\in E$, $\int_{u}^{v}g$ is defined and $z=\int_{u}^{v}g$" on $g$, $u$, $v$ and $z$ is expressed by a predicative formula.

(ii) Let $K$ be an interval containing two distinct points, let $c\in K$, and let $g:K\to\mathbb{R}$ be a map that is integrable on $[u,v]$ for all $u,v\in K$ with $u<v$. Then $\int_{c}^{u}g$ is defined for every $u\in K$, and there is exactly one map from $K$ to $\mathbb{R}$ with value $\int_{c}^{u}g$ at every $u\in K$, the map $u\mapsto\int_{c}^{u}g$. Likewise, let $a,b\in\mathbb{R}$ with $a<b$, and let $(f_{k})_{k\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) such that, for every $k\in\mathbb{N}$, $f_{k}$ is bounded and integrable on $[a,b]$, with integral $\int_{a}^{b}f_{k}$. Then there is exactly one sequence in $\mathbb{R}$ with term $\int_{a}^{b}f_{k}$ for every $k\in\mathbb{N}$, the sequence $\bigl(\int_{a}^{b}f_{k}\bigr)_{k\in\mathbb{N}}$.