theorem Th54: :: MATRIXJ1:54

for n being Nat
for K being Field
for A1, A2 being Matrix of K
for N being Matrix of n,K st len A1 <> width A1 & N = block_diagonal (<*A1,A2*>,(0. K)) holds
Det N = 0. K