[proofplan] Define an antiderivative $F$ of $f$ by integrating from $a$ to the variable endpoint. Then prove that the composition $F \circ g$ is differentiable on $(\alpha,\beta)$ with derivative $(f \circ g)g'$, taking care of the possible case where $g(t)$ lies at an endpoint of $[a,b]$. Finally apply the [Fundamental Theorem of Calculus](/theorems/632) to $F \circ g$ and use the endpoint conditions $g(\alpha)=a$ and $g(\beta)=b$ to obtain the substitution identity. [/proofplan] [step:Construct an antiderivative of $f$ on $[a,b]$] Since $f: [a,b] \to \mathbb{R}$ is [continuous](/page/Continuity), [FTC Part One](/theorems/190) applies to $f$ on the compact interval $[a,b]$. Define the function \begin{align*} F: [a,b] &\to \mathbb{R} \\ x &\mapsto \int_a^x f(s)\,d\mathcal{L}^1(s). \end{align*} Then $F$ is continuous on $[a,b]$, [differentiable](/page/Derivative) on $(a,b)$, and \begin{align*} F'(x)=f(x) \end{align*} for every $x \in (a,b)$. Moreover, by the definition of $F$, \begin{align*} F(b)-F(a)=\int_a^b f(x)\,d\mathcal{L}^1(x). \end{align*} [/step] [step:Differentiate $F \circ g$ along the path $g$] Define the composition \begin{align*} H: [\alpha,\beta] &\to \mathbb{R} \\ t &\mapsto F(g(t)). \end{align*} We prove that $H$ is differentiable on $(\alpha,\beta)$ and that \begin{align*} H'(t)=f(g(t))g'(t) \end{align*} for every $t \in (\alpha,\beta)$. Fix $t_0 \in (\alpha,\beta)$. If $g(t_0) \in (a,b)$, then $F$ is differentiable at $g(t_0)$ and $g$ is differentiable at $t_0$, so the Chain Rule gives \begin{align*} H'(t_0)=F'(g(t_0))g'(t_0)=f(g(t_0))g'(t_0). \end{align*} It remains to handle the endpoint cases. Suppose $g(t_0)=a$. Since $g([\alpha,\beta]) \subset [a,b]$, the point $t_0$ is a local minimum of $g$ relative to the open interval $(\alpha,\beta)$, hence $g'(t_0)=0$ by Fermat's Theorem for Stationary Points. For $t$ near $t_0$ with $t \ne t_0$, write \begin{align*} \frac{H(t)-H(t_0)}{t-t_0} = \frac{F(g(t))-F(a)}{t-t_0}. \end{align*} If $g(t)=a$, this quotient is $0$. If $g(t)>a$, then \begin{align*} \frac{F(g(t))-F(a)}{t-t_0} = \frac{F(g(t))-F(a)}{g(t)-a}\cdot \frac{g(t)-a}{t-t_0}. \end{align*} The first factor tends to $f(a)$ by the one-sided endpoint form of FTC Part One, and the second factor tends to $g'(t_0)=0$. Therefore $H'(t_0)=0=f(a)g'(t_0)=f(g(t_0))g'(t_0)$. The case $g(t_0)=b$ is identical with $t_0$ a local maximum of $g$. Then $g'(t_0)=0$, and the same difference-quotient argument using the left endpoint derivative of $F$ at $b$ gives \begin{align*} H'(t_0)=0=f(b)g'(t_0)=f(g(t_0))g'(t_0). \end{align*} Thus \begin{align*} H'(t)=f(g(t))g'(t) \end{align*} for every $t \in (\alpha,\beta)$. [guided] Define \begin{align*} H: [\alpha,\beta] &\to \mathbb{R} \\ t &\mapsto F(g(t)). \end{align*} The goal is to justify the derivative formula for $H$. If $g(t)$ always stayed inside the open interval $(a,b)$, the ordinary chain rule would finish the step immediately. The only point needing care is that $g(t)$ may equal $a$ or $b$, where $F$ is defined on a closed interval and the derivative of $F$ is only directly supplied in the interior by FTC Part One. Fix $t_0 \in (\alpha,\beta)$. First assume $g(t_0) \in (a,b)$. Since $F$ is differentiable at $g(t_0)$ and $g$ is differentiable at $t_0$, the Chain Rule applies to the composition $F \circ g$ at $t_0$. Using $F'(x)=f(x)$ for $x \in (a,b)$, we get \begin{align*} H'(t_0)=F'(g(t_0))g'(t_0)=f(g(t_0))g'(t_0). \end{align*} Now suppose $g(t_0)=a$. Because $g$ maps all of $[\alpha,\beta]$ into $[a,b]$, no nearby value of $g$ can be less than $a$. Thus $t_0$ is a local minimum of $g$ inside the interval $(\alpha,\beta)$. Since $g$ is differentiable at $t_0$, Fermat's Theorem for Stationary Points gives \begin{align*} g'(t_0)=0. \end{align*} We compute the derivative of $H$ directly from the difference quotient. For $t \ne t_0$ near $t_0$, \begin{align*} \frac{H(t)-H(t_0)}{t-t_0} = \frac{F(g(t))-F(a)}{t-t_0}. \end{align*} If $g(t)=a$, this quotient equals $0$. If $g(t)>a$, then we factor it as \begin{align*} \frac{F(g(t))-F(a)}{t-t_0} = \frac{F(g(t))-F(a)}{g(t)-a}\cdot \frac{g(t)-a}{t-t_0}. \end{align*} The first factor tends to $f(a)$ by the one-sided endpoint derivative obtained from FTC Part One, because \begin{align*} F(x)=\int_a^x f(s)\,d\mathcal{L}^1(s) \end{align*} and $f$ is continuous at $a$. The second factor tends to $g'(t_0)=0$. Hence the product tends to $0$, so \begin{align*} H'(t_0)=0=f(a)g'(t_0)=f(g(t_0))g'(t_0). \end{align*} The case $g(t_0)=b$ is handled in the same way, with $t_0$ a local maximum of $g$ because $g([\alpha,\beta]) \subset [a,b]$. Fermat's theorem gives $g'(t_0)=0$, and the left endpoint derivative of $F$ at $b$ gives \begin{align*} H'(t_0)=0=f(b)g'(t_0)=f(g(t_0))g'(t_0). \end{align*} Combining the interior case and the two endpoint cases proves \begin{align*} H'(t)=f(g(t))g'(t) \end{align*} for every $t \in (\alpha,\beta)$. [/guided] [/step] [step:Apply the Fundamental Theorem of Calculus to $F \circ g$] The function $g$ is continuously differentiable on $[\alpha,\beta]$, and $f \circ g$ is continuous on $[\alpha,\beta]$ because $f$ and $g$ are continuous. Hence the function \begin{align*} [\alpha,\beta] &\to \mathbb{R} \\ t &\mapsto f(g(t))g'(t) \end{align*} is continuous on $[\alpha,\beta]$. Since $H'(t)=f(g(t))g'(t)$ for $t \in (\alpha,\beta)$, the function $H$ is continuously differentiable on $[\alpha,\beta]$ in the sense required by [FTC Part Two](/theorems/191). Therefore \begin{align*} \int_\alpha^\beta f(g(t))g'(t)\,d\mathcal{L}^1(t) &= \int_\alpha^\beta H'(t)\,d\mathcal{L}^1(t) \\ &= H(\beta)-H(\alpha) \\ &= F(g(\beta))-F(g(\alpha)). \end{align*} Using the endpoint hypotheses $g(\alpha)=a$ and $g(\beta)=b$, this becomes \begin{align*} \int_\alpha^\beta f(g(t))g'(t)\,d\mathcal{L}^1(t) = F(b)-F(a). \end{align*} [/step] [step:Recover the original [integral](/page/Integral) from the antiderivative endpoints] By the definition of $F$, \begin{align*} F(b)-F(a) &= \int_a^b f(x)\,d\mathcal{L}^1(x)-\int_a^a f(x)\,d\mathcal{L}^1(x) \\ &= \int_a^b f(x)\,d\mathcal{L}^1(x). \end{align*} Combining this identity with the previous step gives \begin{align*} \int_a^b f(x)\,d\mathcal{L}^1(x) = \int_\alpha^\beta f(g(t))g'(t)\,d\mathcal{L}^1(t). \end{align*} This is the asserted substitution formula, with $d\mathcal{L}^1(x)$ and $d\mathcal{L}^1(t)$ written explicitly for the one-dimensional measures denoted informally by $dx$ and $dt$. [/step]