let D be non empty set ; :: thesis: for d being Element of D
for M being Matrix of D holds block_diagonal (<*M*>,d) = M
let d be Element of D; :: thesis: for M being Matrix of D holds block_diagonal (<*M*>,d) = M
let M be Matrix of D; :: thesis: block_diagonal (<*M*>,d) = M
reconsider E = <*> ((D *) *) as Matrix-yielding FinSequence of (D *) * by Th12;
set ME = <*M*> ^ E;
set B = block_diagonal (<*M*>,d);
A1: len (block_diagonal (<*M*>,d)) = Sum (Len <*M*>) by Def5
.= len M by Lm4 ;
A2: width (block_diagonal (<*M*>,d)) = Sum (Width <*M*>) by Def5
.= width M by Lm5 ;
<*M*> ^ E = <*M*> by FINSEQ_1:34;
hence M = Segm ((block_diagonal (<*M*>,d)),(Seg (len M)),(Seg (width M))) by Th32
.= block_diagonal (<*M*>,d) by A1, A2, MATRIX13:46 ;
:: thesis: verum