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:47;
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