"Special case of a general theorem of Lagrange" doesn't sound well to me: Wikipedia writes that "Lagrange (1773) treated determinants of the second and third order. Lagrange was the first to apply determinants to questions of elimination theory; he proved many special cases of general identities.", so I think your original question is already more general than anything Lagrange has done.

Here are two simple generalizations of your original question:

(1) If

$\left(\begin{array}{cccc}A_{1,1}&A_{1,2}&\dots &A_{1,n} \\\ A_{2,1}&A_{2,2}&\dots &A_{2,n}\\\ \vdots &\vdots &\ddots &\vdots \\\ A_{n,1}&A_{n,2}&\dots &A_{n,n}\end{array}\right)$

is a block matrix with

$A_{i,j}=0$ for every $i < j$, and
$A_{i,i}$ being a square matrix for every $i$,

then its determinant is $\det A_{1,1}\cdot \det A_{2,2}\cdot \dots \cdot \det A_{n,n}$.

The easiest proof (imho) uses the Leibniz formula for determinants, which reduces it to the following combinatorial fact: If a finite set $S$ is the union of some pairwise disjoint sets $S_1$, $S_2$, ..., $S_n$, and $\pi$ is a permutation of the set $S$, then either $\pi\left(S_i\right)=S_i$ for every $i$, or there exist $i < j$ such that $\pi$ maps at least one element of $S_j$ into $S_i$. This is an exercise in induction.

(2) Another generalization: If $\left(U_i\right)_{i\in\mathbb Z}$ is an exact chain complex of finite-dimensional vector spaces, bounded from below and from above (i. e., the vector space $U_i$ is zero for all sufficiently large $i$ and for all sufficiently small $i$), and $\left(f_i\right)_{i\in\mathbb Z}$ is a chain homomorphism from $\left(U_i\right)_{i\in\mathbb Z}$ to $\left(U_i\right)_{i\in\mathbb Z}$, then

$\prod\limits_{i\in\mathbb{Z};\ i\text{ is even}}\det f_i=\prod\limits_{i\in\mathbb{Z};\ i\text{ is odd}}\det f_i$.