let D be non empty set ; :: thesis: 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))))
let d be Element of D; :: thesis: 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))))
let M be Matrix of D; :: thesis: 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))))
let F be FinSequence_of_Matrix of D; :: thesis: 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))))
set FM = F ^ <*M*>;
set L = Len (F ^ <*M*>);
set W = Width (F ^ <*M*>);
set 1F = 1 + (len F);
A1: (1 + (len F)) -' 1 = (1 + (len F)) - 1 by NAT_D:37;
( Len (F ^ <*M*>) = (Len F) ^ (Len <*M*>) & Width (F ^ <*M*>) = (Width F) ^ (Width <*M*>) & len (Len F) = len F & len (Width F) = len F & Len <*M*> = <*(len M)*> & Width <*M*> = <*(width M)*> ) by Th14, Th15, Th18, Th19, FINSEQ_1:def 18;
then A2: ( (Len (F ^ <*M*>)) | (len F) = Len F & (Width (F ^ <*M*>)) | (len F) = Width F & Sum (Len (F ^ <*M*>)) = (Sum (Len F)) + (len M) & Sum (Width (F ^ <*M*>)) = (Sum (Width F)) + (width M) ) by FINSEQ_5:26, RVSUM_1:104;
( 1 + (len F) in Seg ((len F) + 1) & len (F ^ <*M*>) = 1 + (len F) & len (Width (F ^ <*M*>)) = len (F ^ <*M*>) & len (Len (F ^ <*M*>)) = len (F ^ <*M*>) ) by FINSEQ_1:6, FINSEQ_1:def 18, FINSEQ_2:19;
then ( 1 + (len F) in dom (F ^ <*M*>) & (F ^ <*M*>) . (1 + (len F)) = M & (Width (F ^ <*M*>)) | (1 + (len F)) = Width (F ^ <*M*>) & (Len (F ^ <*M*>)) | (1 + (len F)) = Len (F ^ <*M*>) ) by FINSEQ_1:59, FINSEQ_1:79, FINSEQ_1:def 3;
hence 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)))) by A1, A2, Th31; :: thesis: verum