theorem :: MATRIXJ1:55

for n being Nat
for K being Field
for G being FinSequence_of_Matrix of K st Len G <> Width G holds
for M being Matrix of n,K st M = block_diagonal (G,(0. K)) holds
Det M = 0. K