theorem :: MATRIXJ1:79

for K being Field
for R1, R2 being FinSequence_of_Square-Matrix of K st Width R1 = Len R2 holds
(block_diagonal (R1,(0. K))) * (block_diagonal (R2,(0. K))) = block_diagonal ((R1 (#) R2),(0. K))