Proof of Chain Rule for Real Functions on Intervals

Continuity at a point relative to $I$ or to $J$ is read as in The Real Line: Standing Notation and Background for Calculus on Intervals (vi). Put $y=f(x)\in J$.

Increment maps. By Derivative of a Real Function on an Interval (ii), $f'(x)$ is a derivative of $f$ at $x$ and $g'(y)$ is a derivative of $g$ at $y$. By The Increment Form of the Derivative, and Differentiability Implies Continuity (i), applied to $I$, $f$ and $x$, there is a map $\varphi:I\to\mathbb{R}$, continuous at $x$ relative to $I$, with $\varphi(x)=f'(x)$ and $f(t)-f(x)=\varphi(t)\,(t-x)$ for every $t\in I$; and by the same clause, applied to $J$, $g$ and $y$, there is a map $\psi:J\to\mathbb{R}$, continuous at $y$ relative to $J$, with $\psi(y)=g'(y)$ and $g(s)-g(y)=\psi(s)\,(s-y)$ for every $s\in J$. By The Increment Form of the Derivative, and Differentiability Implies Continuity (ii), $f$ is continuous at $x$ relative to $I$.

The map $\psi\circ f$. By Continuity of Identity Maps, Compositions and Reciprocals (ii), applied with $(X,d_{X})=(Y,d_{Y})=(Z,d_{Z})=(\mathbb{R},d_{\mathbb{R}})$, $A=I$, $B=J$, our $f$ and $\psi$ for its $f$ and $g$, and our $x$, the composition $\psi\circ f:I\to\mathbb{R}$, with $(\psi\circ f)(t)=\psi(f(t))$ for $t\in I$, is continuous at $x$ relative to $I$: $f(t)\in J$ for every $t\in I$, $f$ is continuous at $x$ relative to $I$, and $\psi$ is continuous at $f(x)=y$ relative to $J$.

The increment of $g\circ f$. For $t\in I$, applying the identity for $\psi$ with $s=f(t)\in J$ and then the identity for $\varphi$,

$$(g\circ f)(t)-(g\circ f)(x)=g(f(t))-g(y)=\psi(f(t))\,\bigl(f(t)-f(x)\bigr)=\bigl(\psi(f(t))\,\varphi(t)\bigr)(t-x).$$

Let $\theta=(\psi\circ f)\varphi$ be the pointwise product of Pointwise Operations on Real-Valued Maps (i). It is continuous at $x$ relative to $I$ by Continuity of Sums and Products of Real-Valued Functions on a Metric Space (iii), applied in $(\mathbb{R},d_{\mathbb{R}})$ with the subset $I$ to $\psi\circ f$ and $\varphi$; the product formed there is $\theta$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv)). Moreover $\theta(x)=\psi(y)\,\varphi(x)=g'(f(x))\,f'(x)$, and $(g\circ f)(t)-(g\circ f)(x)=\theta(t)\,(t-x)$ for every $t\in I$.

Conclusion. By The Increment Form of the Derivative, and Differentiability Implies Continuity (i), applied to $I$, $g\circ f$, $x$ and $L=g'(f(x))\,f'(x)$, the number $L$ is a derivative of $g\circ f$ at $x$. So $g\circ f$ is differentiable at $x$ by Derivative of a Real Function on an Interval (ii), and $(g\circ f)'(x)$ and $L$ are both derivatives of $g\circ f$ at $x$, so $(g\circ f)'(x)=g'(f(x))\,f'(x)$ by Uniqueness of the Derivative of a Real Function on an Interval (i). This is (i).