theorem Th33: :: MATRIXJ1:33

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 holds M = Segm ((block_diagonal ((F ^ <*M*>),d)),((Seg ((len M) + (Sum (Len F)))) \ (Seg (Sum (Len F)))),((Seg ((width M) + (Sum (Width F)))) \ (Seg (Sum (Width F)))))