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:102;
A2:
Seg (Sum ((Width (<*M*> ^ F)) | 0 )) = {}
by RVSUM_1:102;
A3:
Len <*M*> = <*(len M)*>
by Th15;
A4:
len <*(len M)*> = 1
by FINSEQ_1:56;
Len (<*M*> ^ F) = (Len <*M*>) ^ (Len F)
by Th14;
then
(Len (<*M*> ^ F)) | 1 = <*(len M)*>
by A3, A4, FINSEQ_5:26;
then A5:
Sum ((Len (<*M*> ^ F)) | 1) = len M
by RVSUM_1:103;
A6:
len <*(width M)*> = 1
by FINSEQ_1:56;
A7:
Width <*M*> = <*(width M)*>
by Th19;
A8:
(<*M*> ^ F) . 1 = M
by FINSEQ_1:58;
1 in Seg 1
;
then A9:
1 in dom <*M*>
by FINSEQ_1:55;
A10:
dom <*M*> c= dom (<*M*> ^ F)
by FINSEQ_1:39;
Width (<*M*> ^ F) = (Width <*M*>) ^ (Width F)
by Th18;
then A11:
(Width (<*M*> ^ F)) | 1 = <*(width M)*>
by A7, A6, FINSEQ_5:26;
1 -' 1 = 0
by XREAL_1:234;
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:103
;
verum