Integration by Substitution on a Closed Interval

In the setting of The Real Line: Standing Notation and Background for Calculus on Intervals, let $a,b\in\mathbb{R}$ with $a<b$. Derivatives of maps $[a,b]\to\mathbb{R}$ are taken relative to $[a,b]$, an interval containing two distinct points by Basic Facts about Intervals of the Real Line (v). Let $\varphi:[a,b]\to\mathbb{R}$ be differentiable, with derivative $\varphi':[a,b]\to\mathbb{R}$ continuous on $[a,b]$. Let $J$ be an interval containing two distinct points with $\varphi(t)\in J$ for every $t\in[a,b]$, and let $f:J\to\mathbb{R}$ be continuous on $J$. Let $g:[a,b]\to\mathbb{R}$ be the map $g(t)=f(\varphi(t))\,\varphi'(t)$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v)).

(i) For all $u,v\in J$ with $u<v$, $f$ is integrable on $[u,v]$; so the integral $\int_{u}^{v}f$ of The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vi) and The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vii) is defined, as in The Riemann Integral on a Closed Interval via Lower and Upper Integrals (viii), for all $u,v\in J$.

(ii) $g$ is bounded and integrable on $[a,b]$.

(iii)

$$\int_{a}^{b}f(\varphi(t))\,\varphi'(t)\,dt=\int_{\varphi(a)}^{\varphi(b)}f ,$$

where $\int_{\varphi(a)}^{\varphi(b)}f$ is defined by (i), as $\varphi(a),\varphi(b)\in J$.