theorem Th36: :: MATRIXJ1:36

for D being non empty set
for d being Element of D
for F1, F2 being FinSequence_of_Matrix of D holds block_diagonal ((F1 ^ F2),d) = block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)