theorem :: MATRIXJ1:53

for K being Field
for R being FinSequence_of_Square-Matrix of K holds Det (block_diagonal (R,(0. K))) = Product (Det R)