Maps Given by Integrals of Vector- and Matrix-Valued Maps

In the settings of Single-Variable Calculus on an Interval and Euclidean Space and Real Matrices: Standing Notation, let $p,q\in\mathbb{N}$, let $E\subseteq\mathbb{R}$, let $c\in E$ and let $S\subseteq E$. Integrals of maps $E\to\mathbb{R}^{q}$ and $E\to\mathcal{M}_{p\times q}(\mathbb{R})$, and their being defined, are as in Riemann Integral of a Vector-Valued or Matrix-Valued Map (ii) and Riemann Integral of a Vector-Valued or Matrix-Valued Map (iv). 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); (iii) is a statement of the metatheory.

(i) Let $x:E\to\mathbb{R}^{q}$ be a map such that $\int_{c}^{t}x$ is defined for every $t\in S$. Then there is exactly one map $X:S\to\mathbb{R}^{q}$ with $X(t)=\int_{c}^{t}x$ for every $t\in S$.

(ii) Let $A:E\to\mathcal{M}_{p\times q}(\mathbb{R})$ be a map such that $\int_{c}^{t}A$ is defined for every $t\in S$. Then there is exactly one map $B:S\to\mathcal{M}_{p\times q}(\mathbb{R})$ with $B(t)=\int_{c}^{t}A$ for every $t\in S$.

(iii) The letters $x$, $u$, $v$ and $y$ 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}$, and $[q]$, $\mathbb{R}^{q}$, $[p]\times[q]$ and $\mathcal{M}_{p\times q}(\mathbb{R})$ are parameters. Then the condition "$x$ is a map $x:E\to\mathbb{R}^{q}$, $u,v\in E$, $\int_{u}^{v}x$ is defined and $y=\int_{u}^{v}x$" on $x$, $u$, $v$ and $y$ is expressed by a predicative formula, and so is the condition "$x$ is a map $x:E\to\mathcal{M}_{p\times q}(\mathbb{R})$, $u,v\in E$, $\int_{u}^{v}x$ is defined and $y=\int_{u}^{v}x$".