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 (<*M*> ^ F),d),(Seg (len M)),(Seg (width M))
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 (<*M*> ^ F),d),(Seg (len M)),(Seg (width M))
let M be Matrix of D; :: thesis: for F being FinSequence_of_Matrix of D holds M = Segm (block_diagonal (<*M*> ^ F),d),(Seg (len M)),(Seg (width M))
let F be FinSequence_of_Matrix of D; :: thesis: M = Segm (block_diagonal (<*M*> ^ F),d),(Seg (len M)),(Seg (width M))
set MF = <*M*> ^ F;
set L = Len (<*M*> ^ F);
set W = Width (<*M*> ^ F);
A1: 1 -' 1 = 0 by XREAL_1:234;
A2: ( Seg (Sum ((Len (<*M*> ^ F)) | 0 )) = {} & Seg (Sum ((Width (<*M*> ^ F)) | 0 )) = {} ) by RVSUM_1:102;
( Len (<*M*> ^ F) = (Len <*M*>) ^ (Len F) & Len <*M*> = <*(len M)*> & len <*(len M)*> = 1 & Width (<*M*> ^ F) = (Width <*M*>) ^ (Width F) & Width <*M*> = <*(width M)*> & len <*(width M)*> = 1 ) by Th14, Th18, Th15, Th19, FINSEQ_1:56;
then ( (Len (<*M*> ^ F)) | 1 = <*(len M)*> & (Width (<*M*> ^ F)) | 1 = <*(width M)*> ) by FINSEQ_5:26;
then A3: ( Sum ((Len (<*M*> ^ F)) | 1) = len M & Sum ((Width (<*M*> ^ F)) | 1) = width M ) by RVSUM_1:103;
1 in Seg 1 ;
then ( 1 in dom <*M*> & dom <*M*> c= dom (<*M*> ^ F) ) by FINSEQ_1:39, FINSEQ_1:55;
then ( 1 in dom (<*M*> ^ F) & (<*M*> ^ F) . 1 = M ) by FINSEQ_1:58;
hence M = Segm (block_diagonal (<*M*> ^ F),d),((Seg (Sum ((Len (<*M*> ^ F)) | 1))) \ {} ),((Seg (Sum ((Width (<*M*> ^ F)) | 1))) \ {} ) by A1, Th31, A2
.= Segm (block_diagonal (<*M*> ^ F),d),(Seg (len M)),(Seg (width M)) by A3 ;
:: thesis: verum