[proofplan] The strategy is to expand $\det(A^\top A)$ as a sum over permutations using the Leibniz formula and reindex the resulting double sum by grouping terms according to which $m$-element subset $S \subseteq \{1, \dots, n\}$ of row indices contributes. The Leibniz formula expresses $\det(A^\top A)$ as a sum over $\sigma \in S_m$ of signed products $\prod_j (A^\top A)_{j, \sigma(j)}$. Expanding each entry $(A^\top A)_{j, \sigma(j)} = \sum_i A_{ij} A_{i, \sigma(j)}$ produces a sum over functions $\phi: \{1, \dots, m\} \to \{1, \dots, n\}$. Grouping these functions by their image $S = \phi(\{1, \dots, m\})$ when injective (and noting that non-injective $\phi$ contribute zero by an alternation argument) yields exactly $\sum_S (\det A_S)^2$. The corollary on $\mathbf{J}_m L$ follows by applying the formula with $A = JL$ and using the definition $\mathbf{J}_m L = \sqrt{\det(JL^\top JL)}$. [/proofplan]

[step:Expand $\det(A^\top A)$ via the Leibniz formula] Let $A \in \mathbb{R}^{n \times m}$ with $m \le n$, and write $A_{ij}$ for the entry in row $i \in \{1, \dots, n\}$ and column $j \in \{1, \dots, m\}$. The Gram matrix $B := A^\top A \in \mathbb{R}^{m \times m}$ has entries \begin{align*} B_{jk} = (A^\top A)_{jk} = \sum_{i=1}^n A_{ij} A_{ik}, \qquad j, k \in \{1, \dots, m\}. \end{align*} The Leibniz formula for the determinant of an $m \times m$ matrix $B$ is \begin{align*} \det B = \sum_{\sigma \in S_m} \operatorname{sgn}(\sigma) \prod_{j=1}^m B_{j, \sigma(j)}, \end{align*} where $S_m$ is the symmetric group on $\{1, \dots, m\}$ and $\operatorname{sgn}(\sigma) \in \{+1, -1\}$ is the sign of the permutation $\sigma$. Substituting the expansion of $B_{j, \sigma(j)}$ and using multilinearity: \begin{align*} \det(A^\top A) = \sum_{\sigma \in S_m} \operatorname{sgn}(\sigma) \prod_{j=1}^m \left(\sum_{i_j=1}^n A_{i_j, j} A_{i_j, \sigma(j)}\right). \end{align*} Distributing the product over the sums (a finite expansion), the right-hand side becomes \begin{align*} \det(A^\top A) = \sum_{\sigma \in S_m} \operatorname{sgn}(\sigma) \sum_{\phi: \{1,\dots,m\} \to \{1,\dots,n\}} \prod_{j=1}^m A_{\phi(j), j} A_{\phi(j), \sigma(j)}, \end{align*} where the inner sum runs over all functions $\phi: \{1, \dots, m\} \to \{1, \dots, n\}$ (we replaced the indices $i_1, \dots, i_m$ by the function $\phi$ with $\phi(j) = i_j$). [/step]

[step:Show that non-injective $\phi$ contribute zero by symmetry] We swap the order of summation: \begin{align*} \det(A^\top A) = \sum_{\phi: \{1,\dots,m\} \to \{1,\dots,n\}} \left(\prod_{j=1}^m A_{\phi(j), j}\right) \sum_{\sigma \in S_m} \operatorname{sgn}(\sigma) \prod_{j=1}^m A_{\phi(j), \sigma(j)}. \end{align*} We now claim that any function $\phi$ which is not injective contributes zero to this sum. Suppose $\phi$ is not injective: there exist distinct indices $j_1 \ne j_2$ in $\{1, \dots, m\}$ with $\phi(j_1) = \phi(j_2) =: i$. Let $\tau \in S_m$ be the transposition swapping $j_1$ and $j_2$, with $\operatorname{sgn}(\tau) = -1$. We pair each $\sigma \in S_m$ with $\sigma \circ \tau \in S_m$. The map $\sigma \mapsto \sigma \circ \tau$ is an involution on $S_m$ with $\operatorname{sgn}(\sigma \circ \tau) = -\operatorname{sgn}(\sigma)$. We compare the two products: \begin{align*} \prod_{j=1}^m A_{\phi(j), \sigma(j)} \quad \text{versus} \quad \prod_{j=1}^m A_{\phi(j), (\sigma \circ \tau)(j)}. \end{align*} Reindexing the second product by setting $j' = \tau(j)$ (so $\tau(j') = j$ since $\tau^2 = \mathrm{id}$), \begin{align*} \prod_{j=1}^m A_{\phi(j), (\sigma \circ \tau)(j)} = \prod_{j'=1}^m A_{\phi(\tau(j')), \sigma(j')}. \end{align*} Now $\phi(\tau(j')) = \phi(j')$ for every $j'$: indeed, if $j' \notin \{j_1, j_2\}$ then $\tau(j') = j'$; if $j' = j_1$ then $\tau(j') = j_2$ and $\phi(\tau(j')) = \phi(j_2) = i = \phi(j_1) = \phi(j')$ (similarly for $j' = j_2$). Hence the two products are equal: \begin{align*} \prod_{j=1}^m A_{\phi(j), \sigma(j)} = \prod_{j=1}^m A_{\phi(j), (\sigma \circ \tau)(j)}. \end{align*} Pairing $\sigma$ with $\sigma \circ \tau$, the contributions cancel: \begin{align*} \operatorname{sgn}(\sigma) \prod_j A_{\phi(j), \sigma(j)} + \operatorname{sgn}(\sigma \circ \tau) \prod_j A_{\phi(j), (\sigma \circ \tau)(j)} = (\operatorname{sgn}(\sigma) - \operatorname{sgn}(\sigma)) \prod_j A_{\phi(j), \sigma(j)} = 0. \end{align*} Summing over a complete set of pairs (the involution $\sigma \mapsto \sigma \circ \tau$ has no fixed points since it changes the sign), the inner sum $\sum_{\sigma \in S_m} \operatorname{sgn}(\sigma) \prod_j A_{\phi(j), \sigma(j)}$ vanishes. Hence non-injective $\phi$ contribute zero. [/step]

[step:Group injective $\phi$ by their image $S$ and reduce to determinants of submatrices] Only injective functions $\phi: \{1, \dots, m\} \to \{1, \dots, n\}$ contribute. Each such $\phi$ has an image $S := \phi(\{1, \dots, m\})$ which is an $m$-element subset of $\{1, \dots, n\}$, and $\phi$ factors as a bijection from $\{1, \dots, m\}$ onto $S$. Fix an $m$-element subset $S \subseteq \{1, \dots, n\}$. Let $\iota_S: \{1, \dots, m\} \to S$ denote the unique order-preserving bijection (so $\iota_S(1) < \iota_S(2) < \cdots < \iota_S(m)$ are the elements of $S$ in increasing order). Every injective $\phi$ with image $S$ can be written uniquely as $\phi = \iota_S \circ \pi$ for some permutation $\pi \in S_m$. Submatrix definition: $A_S \in \mathbb{R}^{m \times m}$ is the matrix with $(A_S)_{kj} := A_{\iota_S(k), j}$ for $k, j \in \{1, \dots, m\}$ (the rows of $A$ indexed by $S$, written in the natural order). We collect all injective $\phi$ with image $S$ and compute their joint contribution: \begin{align*} \sum_{\substack{\phi \text{ injective} \\ \phi(\{1,\dots,m\}) = S}} \left(\prod_{j=1}^m A_{\phi(j), j}\right) \sum_{\sigma \in S_m} \operatorname{sgn}(\sigma) \prod_{j=1}^m A_{\phi(j), \sigma(j)}. \end{align*} Substituting $\phi = \iota_S \circ \pi$ with $\pi \in S_m$: \begin{align*} A_{\phi(j), j} = A_{\iota_S(\pi(j)), j} = (A_S)_{\pi(j), j}, \qquad A_{\phi(j), \sigma(j)} = (A_S)_{\pi(j), \sigma(j)}. \end{align*} Hence \begin{align*} \sum_{\pi \in S_m} \prod_{j=1}^m (A_S)_{\pi(j), j} \cdot \sum_{\sigma \in S_m} \operatorname{sgn}(\sigma) \prod_{j=1}^m (A_S)_{\pi(j), \sigma(j)}. \end{align*} We compute the inner sum first. Reindex by $k := \pi(j)$ (so $j = \pi^{-1}(k)$); since $\pi$ is a bijection, \begin{align*} \prod_{j=1}^m (A_S)_{\pi(j), \sigma(j)} = \prod_{k=1}^m (A_S)_{k, \sigma(\pi^{-1}(k))} = \prod_{k=1}^m (A_S)_{k, (\sigma \circ \pi^{-1})(k)}. \end{align*} Setting $\tau := \sigma \circ \pi^{-1} \in S_m$ (a bijection of $S_m$ for each fixed $\pi$, with $\operatorname{sgn}(\tau) = \operatorname{sgn}(\sigma) \operatorname{sgn}(\pi^{-1}) = \operatorname{sgn}(\sigma) \operatorname{sgn}(\pi)$), so $\operatorname{sgn}(\sigma) = \operatorname{sgn}(\tau) \operatorname{sgn}(\pi)$. As $\sigma$ ranges over $S_m$ for fixed $\pi$, so does $\tau$: \begin{align*} \sum_{\sigma \in S_m} \operatorname{sgn}(\sigma) \prod_{j=1}^m (A_S)_{\pi(j), \sigma(j)} = \operatorname{sgn}(\pi) \sum_{\tau \in S_m} \operatorname{sgn}(\tau) \prod_{k=1}^m (A_S)_{k, \tau(k)} = \operatorname{sgn}(\pi) \det(A_S), \end{align*} where the last step is again the Leibniz formula applied to $A_S$. Substituting back, the contribution from subset $S$ becomes \begin{align*} \sum_{\pi \in S_m} \prod_{j=1}^m (A_S)_{\pi(j), j} \cdot \operatorname{sgn}(\pi) \det(A_S) = \det(A_S) \sum_{\pi \in S_m} \operatorname{sgn}(\pi) \prod_{j=1}^m (A_S)_{\pi(j), j}. \end{align*} The remaining sum is once again the Leibniz formula for $\det(A_S)$ (applied with the role of row/column index swapped, which gives the same value since $\det(A_S^\top) = \det(A_S)$): \begin{align*} \sum_{\pi \in S_m} \operatorname{sgn}(\pi) \prod_{j=1}^m (A_S)_{\pi(j), j} = \det(A_S). \end{align*} Hence the total contribution from subset $S$ is $(\det A_S)^2$. [/step]

[step:Sum over all $m$-element subsets to obtain the Cauchy–Binet identity] Combining the previous steps, \begin{align*} \det(A^\top A) = \sum_{\substack{S \subseteq \{1, \dots, n\} \\ |S| = m}} (\det A_S)^2, \end{align*} which is the Cauchy–Binet identity. The sum has $\binom{n}{m}$ terms, one for each $m$-element subset $S \subseteq \{1, \dots, n\}$. For the corollary on the $m$-dimensional Jacobian: applying the identity with $A = JL$ and recalling the definition $\mathbf{J}_m L = \sqrt{\det(JL^\top JL)}$, \begin{align*} \mathbf{J}_m L = \sqrt{\det(JL^\top JL)} = \sqrt{\sum_{\substack{S \subseteq \{1,\dots,n\} \\ |S| = m}} (\det (JL)_S)^2}. \end{align*} The square root is well-defined because the right-hand side is a sum of squares of real numbers, hence non-negative. [/step]