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 st M = {} holds
( block_diagonal (F ^ <*M*>),d = block_diagonal F,d & block_diagonal (<*M*> ^ F),d = block_diagonal F,d )
let d be Element of D; :: thesis: for M being Matrix of D
for F being FinSequence_of_Matrix of D st M = {} holds
( block_diagonal (F ^ <*M*>),d = block_diagonal F,d & block_diagonal (<*M*> ^ F),d = block_diagonal F,d )
let M be Matrix of D; :: thesis: for F being FinSequence_of_Matrix of D st M = {} holds
( block_diagonal (F ^ <*M*>),d = block_diagonal F,d & block_diagonal (<*M*> ^ F),d = block_diagonal F,d )
let F be FinSequence_of_Matrix of D; :: thesis: ( M = {} implies ( block_diagonal (F ^ <*M*>),d = block_diagonal F,d & block_diagonal (<*M*> ^ F),d = block_diagonal F,d ) )
assume A1: M = {} ; :: thesis: ( block_diagonal (F ^ <*M*>),d = block_diagonal F,d & block_diagonal (<*M*> ^ F),d = block_diagonal F,d )
set MM = <*M*>;
set bf = block_diagonal F,d;
set BF = <*(block_diagonal F,d)*>;
set bFM = block_diagonal (<*(block_diagonal F,d)*> ^ <*M*>),d;
set bMF = block_diagonal (<*M*> ^ <*(block_diagonal F,d)*>),d;
set BFM = block_diagonal (F ^ <*M*>),d;
set BMF = block_diagonal (<*M*> ^ F),d;
A2: len M = 0 by A1;
A3: width M = 0 by A1, CARD_1:47, MATRIX_1:def 4;
A4: ( len (block_diagonal (<*(block_diagonal F,d)*> ^ <*M*>),d) = Sum (Len (<*(block_diagonal F,d)*> ^ <*M*>)) & len (block_diagonal (<*M*> ^ <*(block_diagonal F,d)*>),d) = Sum (Len (<*M*> ^ <*(block_diagonal F,d)*>)) & width (block_diagonal (<*(block_diagonal F,d)*> ^ <*M*>),d) = Sum (Width (<*(block_diagonal F,d)*> ^ <*M*>)) & width (block_diagonal (<*M*> ^ <*(block_diagonal F,d)*>),d) = Sum (Width (<*M*> ^ <*(block_diagonal F,d)*>)) ) by Def5;
( Len (<*(block_diagonal F,d)*> ^ <*M*>) = (Len <*(block_diagonal F,d)*>) ^ (Len <*M*>) & Len (<*M*> ^ <*(block_diagonal F,d)*>) = (Len <*M*>) ^ (Len <*(block_diagonal F,d)*>) & Sum (Len <*M*>) = len M & Width (<*(block_diagonal F,d)*> ^ <*M*>) = (Width <*(block_diagonal F,d)*>) ^ (Width <*M*>) & Width (<*M*> ^ <*(block_diagonal F,d)*>) = (Width <*M*>) ^ (Width <*(block_diagonal F,d)*>) & Sum (Width <*M*>) = width M & Sum (Len <*(block_diagonal F,d)*>) = len (block_diagonal F,d) & Sum (Width <*(block_diagonal F,d)*>) = width (block_diagonal F,d) ) by Th14, Th18, Lm4, Lm5;
then A5: ( len (block_diagonal (<*(block_diagonal F,d)*> ^ <*M*>),d) = (len (block_diagonal F,d)) + (len M) & len (block_diagonal (<*M*> ^ <*(block_diagonal F,d)*>),d) = (len M) + (len (block_diagonal F,d)) & width (block_diagonal (<*(block_diagonal F,d)*> ^ <*M*>),d) = (width (block_diagonal F,d)) + (width M) & width (block_diagonal (<*M*> ^ <*(block_diagonal F,d)*>),d) = (width M) + (width (block_diagonal F,d)) ) by A4, RVSUM_1:105;
A6: ( Sum (Len <*M*>) = 0 & Sum (Width <*M*>) = 0 ) by A2, A3, Lm4, Lm5;
thus block_diagonal (F ^ <*M*>),d = block_diagonal (<*(block_diagonal F,d)*> ^ <*M*>),d by Th35
.= Segm (block_diagonal (<*(block_diagonal F,d)*> ^ <*M*>),d),(Seg (len (block_diagonal (<*(block_diagonal F,d)*> ^ <*M*>),d))),(Seg (width (block_diagonal (<*(block_diagonal F,d)*> ^ <*M*>),d))) by MATRIX13:46
.= block_diagonal F,d by Th32, A5, A2, A3 ; :: thesis: block_diagonal (<*M*> ^ F),d = block_diagonal F,d
thus block_diagonal (<*M*> ^ F),d = block_diagonal (<*M*> ^ <*(block_diagonal F,d)*>),d by Th36
.= Segm (block_diagonal (<*M*> ^ <*(block_diagonal F,d)*>),d),(Seg (len (block_diagonal (<*M*> ^ <*(block_diagonal F,d)*>),d))),(Seg (width (block_diagonal (<*M*> ^ <*(block_diagonal F,d)*>),d))) by MATRIX13:46
.= Segm (block_diagonal (<*M*> ^ <*(block_diagonal F,d)*>),d),((Seg ((len (block_diagonal F,d)) + (Sum (Len <*M*>)))) \ (Seg (Sum (Len <*M*>)))),((Seg ((width (block_diagonal F,d)) + (Sum (Width <*M*>)))) \ (Seg (Sum (Width <*M*>)))) by A2, A5, A6, FINSEQ_1:4, MATRIX_1:def 4
.= block_diagonal F,d by Th33 ; :: thesis: verum