theorem Th32: :: MATRIXJ1:32

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 ((<*M*> ^ F),d)),(Seg (len M)),(Seg (width M)))