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 ((<*M*> ^ F),d)),(Seg (len M)),(Seg (width M)))
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 ((<*M*> ^ F),d)),(Seg (len M)),(Seg (width M)))
let M be 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 F be FinSequence_of_Matrix of D; 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:
Seg (Sum ((Len (<*M*> ^ F)) | 0)) = {}
by RVSUM_1:72;
A2:
Seg (Sum ((Width (<*M*> ^ F)) | 0)) = {}
by RVSUM_1:72;
A3:
Len <*M*> = <*(len M)*>
by Th15;
A4:
len <*(len M)*> = 1
by FINSEQ_1:39;
Len (<*M*> ^ F) = (Len <*M*>) ^ (Len F)
by Th14;
then
(Len (<*M*> ^ F)) | 1 = <*(len M)*>
by A3, A4, FINSEQ_5:23;
then A5:
Sum ((Len (<*M*> ^ F)) | 1) = len M
by RVSUM_1:73;
A6:
len <*(width M)*> = 1
by FINSEQ_1:39;
A7:
Width <*M*> = <*(width M)*>
by Th19;
A8:
(<*M*> ^ F) . 1 = M
by FINSEQ_1:41;
1 in Seg 1
;
then A9:
1 in dom <*M*>
by FINSEQ_1:38;
A10:
dom <*M*> c= dom (<*M*> ^ F)
by FINSEQ_1:26;
Width (<*M*> ^ F) = (Width <*M*>) ^ (Width F)
by Th18;
then A11:
(Width (<*M*> ^ F)) | 1 = <*(width M)*>
by A7, A6, FINSEQ_5:23;
1 -' 1 = 0
by XREAL_1:232;
hence M =
Segm ((block_diagonal ((<*M*> ^ F),d)),((Seg (Sum ((Len (<*M*> ^ F)) | 1))) \ {}),((Seg (Sum ((Width (<*M*> ^ F)) | 1))) \ {}))
by A1, A2, A9, A10, A8, Th31
.=
Segm ((block_diagonal ((<*M*> ^ F),d)),(Seg (len M)),(Seg (width M)))
by A11, A5, RVSUM_1:73
;
verum