theorem Th40: :: MATRIXJ1:40

for D being non empty set
for d being Element of D
for M being Matrix of D
for F being FinSequence_of_Matrix of D st M = {} holds
( block_diagonal ((F ^ <*M*>),d) = block_diagonal (F,d) & block_diagonal ((<*M*> ^ F),d) = block_diagonal (F,d) )