How to Prove the Change of Variables Theorem Using Mathematical Induction

Problem

Inductive proof of the change of variables theorem I wanted to drop here an inductive proof of the Change of Variables Theorem (in integration), which might or might not be novel. If I'm not mistaken, MathSE serves as a repository, so self-answered questions are/were allowed (correct me if I'm wrong). If this is not the case, then the question is: has such an inductive proof (that I'm about to present) already been posted or published anywhere? Back to the matter at hand. Induction (on the dimension $n$) works well to prove this theorem by virtue of Fubini's theorem (which enables the nesting of multidimensional integrals into lower-dimensional nested integrals). To get further motivated, let's see the method in action to derive the polar co-ordinate measure from the Cartesian (Lebesgue) measure, provided we only know about 1D change of variables (1D=basis step for our induction): $$dx(dy)\overset{y(\theta)=x\tan(\theta),\,x=\text{ fixed parameter}}{=}(dx)(d\theta)x[\cos(\theta)]^{-2}\overset{\text{'Fubini'}}{=}d\theta(dx\,x[\cos(\theta)]^{-2})=\overset{x(r)=r\cos(\theta),\,\theta=\text{ fixed parameter}}{=}(dr)(d\theta)r$$ Since this idea is so simple, the underlying proof strategy so easy to memorize and the method generalizes to a general proof for the change of variables theorem, I found it worthwhile to flesh out the details and compose such a proof. Lemma 1 Suppose $U\subseteq\mathbb{R}^n$ is open, $f:U \to \mathbb{R}^+$ an integrable function, $\sigma\in S^n$ and $\pi:\mathbb{R}^n \to \mathbb{R}^n:x\mapsto (x_{\sigma(1)},...,x_{\sigma(n)})$. Then $$\int_{\pi(U)}d\lambda_n(x)\,f(x)=\int_{U}d\lambda_n(x)\,(f\circ \pi)(x)$$ Lemma 2 Suppose $U\subseteq \mathbb{R}^n$ ($n>1$) is open and $g:U\to \mathbb{R}^n$ a diffeomorphism. The vector-space $C_c(U,\mathbb{R})$ is the linear span of the set \begin{gather*}C_{\text{loc.}}:=\left\{f\in C_c(U,\mathbb{R})|\,\exists\text{ open } V\subseteq U:\exists j\in \{1,...,n\}:\right.\\ \left.\,(V\supset \text{ supp }f)\text{ and }(h:V\mapsto \mathbb{R}^n: x\mapsto (x_1,...,x_{n-1},g_j(x)) \text{ is a diffeomorphism}\right\} \end{gather*} Theorem Let $U,V\subseteq \mathbb{R}^n$ be open, let $g:U \to V$ be a $C^1$ diffeomorphism and $f\in C_c(V,\mathbb{R}^+)$. Then $$\int_{V}d\lambda(x)f(x)=\int_Ud\lambda(y)|\det(dg(y))|\,(f\circ g)(y).$$ Proof We proceed by induction on $n$. The basis step $n=1$, I will omit for this occasion (too standard). Now for the induction step. Let $U,V\subseteq \mathbb{R}^{n}$ ($n>1$) be open and $g:U\to V$ a $C^1$ diffeomorphism. By virtue of Lemma 1 and the linearity of the integral, it suffices to prove the stated theorem for the case where $f\in C_c(V,\mathbb{R}^+)$ has such a `slim' support that $\exists j\in \{1,...,n\}: \exists \text{ open }\tilde{V}\subseteq V:\,\tilde{V}\supseteq \text{supp }f$ and $$h:\underbrace{g^{-1}(\tilde{V})}_{=:\tilde{U}}\to \mathbb{R}:x\mapsto (x_1,...,x_{n-1},g_j(x))\text{ is a $C^1$ diffeomorphism.}$$ To proceed, we still define... $\sigma\in S^n$ the transposition that swaps $j$ and $n$, $\pi:\mathbb{R}^n \to \mathbb{R}^n: x \mapsto (x_{\sigma(1)},\ldots,x_{\sigma(n)})$, $k:=\pi \circ g\circ h^{-1}$, $p_{<n}:\mathbb{R}^n \to \mathbb{R}^{n-1}:x \mapsto (x_1,\ldots,x_{n-1})$, $p_n:\mathbb{R}^n \to \mathbb{R}:x \mapsto x_n$, $\{.,..\}:\mathbb{R}^{n-1}\times \mathbb{R}\mapsto \mathbb{R}^{n}:(y,t)\mapsto \{y,t\}:=(y_1,...,y_{n-1},t)$ a conventient co-ordinate fusion map, and finally... $\forall s \in p_n(h(\tilde{U}))$ we define $$q_s:p_{<n}(h(\tilde{U})\cap p_n^{-1}(s)) \to \mathbb{R}^{n-1}:y\mapsto p_{<n}(k(\{y,s\})).$$ Now note that $\forall x\in \tilde{U}$ we have $(k(h(x)))_n=g_j(x)=h_n(x)$. Since $h$ is one-to-one, we therefore have $\forall y\in h(\tilde{U})$ that $k_n(y)=y_n$. From the identity $k(\{y,s\})\equiv\{q_s(y),s\}$, we deduce that $q_s$ is a diffeomorphism for every $s\in p_n(h(\tilde{U}))$. Now we can proceed with the key computation: \begin{gather*} \int_{V}d\lambda^n(x)\,f(x)=\int_{\tilde{V}}d\lambda^n(x)\,f(x) \overset{\tilde{x}=\pi^{-1}(x),\text{ Lemma 2}, \tilde{f}:=f\circ \pi^{-1}}{=}\int_{\pi(\tilde{V})}d\lambda^n(\tilde{x})\,\tilde{f}(\tilde{x}) \\ \overset{\text{Fubini}}{=} \int_{p_n(\pi(\tilde{V}))}d\lambda(s)\left(\int_{p_{<n}(\pi(\tilde{V}))}d\lambda^{n-1}(\xi)\,\tilde{f}(\{\xi,s\})\right)\\ \overset{\text{ind. hyp.}}{=}\int_{p_n(\pi(\tilde{V}))}d\lambda(s)\left(\int_{q_s^{-1}(p_{<n}(\pi(\tilde{V})))}d\lambda^{n-1}(z)|\det(dq_{s}(z)|\,\tilde{f}(\{q_{s}(z),s\})\right)\\ =\int_{p_n(k^{-1}(\pi(\tilde{V})))}d\lambda(s)\left(\int_{p_{<n}(k^{-1}(\pi(\tilde{V})))}d\lambda^{n-1}(z)|\det(dk(\{z,s\}))|\,\tilde{f}(k(\{z,s\}))\right)\\ \overset{\text{Fubini},\, k^{-1}(\pi(\tilde{V}))=h(\tilde{U})}{=}\int_{p_{<n}(h(\tilde{U}))}d\lambda^{n-1}(z)\left(\int_{p_{n}(h(\tilde{U}))}d\lambda(s)|\det(dk(\{z,s\})|\,\tilde{f}(k(\{z,s\}))\right)\\ \overset{\text{ind. hyp.}}{=}\int_{p_{<n}(h(\tilde{U}))}d\lambda^{n-1}(z)\left(\int_{g_j^{-1}(p_{n}(h(\tilde{U})))}d\lambda_{1}(t)|(\partial_ng_{j}(\{z,t\})||\det(dk(\{z,g_{j}(\{z,t\})\})|\,\tilde{f}(k(\{z,g_{j}(\{z,t\})\}))\right)\\ =\int_{p_{<n}(\tilde{U})}d\lambda^{n-1}(z)\left(\int_{p_{n}(\tilde{U})}d\lambda(t)|\det (dh(\{z,t\})||\det(dk(h(\{z,t\})))|\,\tilde{f}(k(h(\{z,t\})))\right)\\ \overset{(\det A)(det B)=\det(AB),\text{ chain rule},\text{ Fubini}}{=}\int_{\tilde{U}}d\lambda^{n}(y)|\det (d(\pi\circ g)(y))|\,\tilde{f}((\pi\circ g)(y)))\\ =\int_{U}d\lambda^{n}(y)|\det (dg(y))|\,f(g(y))) \end{gather*} EDIT: according to a MSE question popping up in the "related" tab, the book "Integration and probability" from P. Malliavin has a proof using this strategy (page 83).