theorem Th78: :: MATRIXJ1:78

for K being Field
for A1, A2, B1, B2 being Matrix of K st width A1 = len B1 & width A2 = len B2 holds
(block_diagonal (<*A1,A2*>,(0. K))) * (block_diagonal (<*B1,B2*>,(0. K))) = block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K))