Cauchy-Binet formula: general form

In Wikipedia, the Cauchy-Binet formula is stated for determinant of product of matrices $A_{m\times n}$ and $B_{n\times m}$.

However, Handbook of Linear Algebra state the formula (without proof) as

A $k\times k$ minor in product $AB$ can be obtained as sum of products of $k\times k$ minors in $A$ and $k\times k$ minors in $B$. More precisely let $\alpha,\beta,\gamma$ denotes $k$-tuples of increasing sequences of positive integers (within maximum sizes of matrices $A,B$). Let $A[\alpha,\beta]$ denote the $k\times k$ minor of $A$ whose $k$ rows are w.r.t indices in $\alpha$ and $k$ columns are w.r.t. indices in $\beta$. Then $$(AB)[\alpha,\beta] = \sum_{\gamma} A[\alpha,\gamma]B[\gamma,\beta],$$ where sum is over all $k$-tuples $\gamma$ of increasing sequence of positive integers (within maximum sizes of matrices $A,B$).

Q.1 Where can I find the proof of this generalized Cauchy-Binet formula?

In many books of matrices, I didn't find its proof (except proof of determinant expansion of product $AB$- the largest minor when sizes of $A,B$ are dual i.e. if $A$ has size $m\times n$, then $B$ has size $n\times m$.)

Q.2 Can one state some reference or book which contains interesting applications of this formula.

(Let me know if there is anything missing in above expansion formula; you may edit as well for correction.)

• We can see this formula as a consequence of the functoriality of $\Lambda^k$ (the $k$th exterior power). The coefficients of the matrix of $\Lambda^k f$ are the $k×k$ minors of the matrix of $f$. Then, $\Lambda^k (f \circ g) = (\Lambda^k f) \circ (\Lambda^k g)$ translates as the given formula. – Idéophage Mar 5 at 13:30