let D be 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)))))
let d be 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 M be 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 F be FinSequence_of_Matrix of D; 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:
len (F ^ <*M*>) = 1 + (len F)
by FINSEQ_2:16;
len (Len (F ^ <*M*>)) = len (F ^ <*M*>)
by CARD_1:def 7;
then A2:
(Len (F ^ <*M*>)) | (1 + (len F)) = Len (F ^ <*M*>)
by A1, FINSEQ_1:58;
len (Width (F ^ <*M*>)) = len (F ^ <*M*>)
by CARD_1:def 7;
then A3:
(Width (F ^ <*M*>)) | (1 + (len F)) = Width (F ^ <*M*>)
by A1, FINSEQ_1:58;
1 + (len F) in Seg ((len F) + 1)
by FINSEQ_1:4;
then A4:
1 + (len F) in dom (F ^ <*M*>)
by A1, FINSEQ_1:def 3;
A5:
Width (F ^ <*M*>) = (Width F) ^ (Width <*M*>)
by Th18;
len (Width F) = len F
by CARD_1:def 7;
then A6:
(Width (F ^ <*M*>)) | (len F) = Width F
by A5, FINSEQ_5:23;
Width <*M*> = <*(width M)*>
by Th19;
then A7:
Sum (Width (F ^ <*M*>)) = (Sum (Width F)) + (width M)
by A5, RVSUM_1:74;
A8:
Len (F ^ <*M*>) = (Len F) ^ (Len <*M*>)
by Th14;
len (Len F) = len F
by CARD_1:def 7;
then A9:
(Len (F ^ <*M*>)) | (len F) = Len F
by A8, FINSEQ_5:23;
Len <*M*> = <*(len M)*>
by Th15;
then A10:
Sum (Len (F ^ <*M*>)) = (Sum (Len F)) + (len M)
by A8, RVSUM_1:74;
A11:
(F ^ <*M*>) . (1 + (len F)) = M
by FINSEQ_1:42;
(1 + (len F)) -' 1 = (1 + (len F)) - 1
by NAT_D:37;
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 A9, A6, A10, A7, A4, A11, A3, A2, Th31; verum