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 ) )
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;
A1: width (block_diagonal (<*M*> ^ <*(block_diagonal F,d)*>),d) = Sum (Width (<*M*> ^ <*(block_diagonal F,d)*>)) by Def5;
A2: Len (<*(block_diagonal F,d)*> ^ <*M*>) = (Len <*(block_diagonal F,d)*>) ^ (Len <*M*>) by Th14;
A3: Sum (Len <*(block_diagonal F,d)*>) = len (block_diagonal F,d) by Lm4;
assume A4: M = {} ; :: thesis: ( block_diagonal (F ^ <*M*>),d = block_diagonal F,d & block_diagonal (<*M*> ^ F),d = block_diagonal F,d )
then A5: len M = 0 ;
then A6: Sum (Len <*M*>) = 0 by Lm4;
A7: width M = 0 by A4, CARD_1:47, MATRIX_1:def 4;
then A8: Sum (Width <*M*>) = 0 by Lm5;
A9: Sum (Len <*M*>) = len M by Lm4;
then B9: Seg (Sum (Width <*M*>)) = {} by A8;
len (block_diagonal (<*(block_diagonal F,d)*> ^ <*M*>),d) = Sum (Len (<*(block_diagonal F,d)*> ^ <*M*>)) by Def5;
then A10: len (block_diagonal (<*(block_diagonal F,d)*> ^ <*M*>),d) = (len (block_diagonal F,d)) + (len M) by A2, A9, A3, RVSUM_1:105;
A11: Len (<*M*> ^ <*(block_diagonal F,d)*>) = (Len <*M*>) ^ (Len <*(block_diagonal F,d)*>) by Th14;
len (block_diagonal (<*M*> ^ <*(block_diagonal F,d)*>),d) = Sum (Len (<*M*> ^ <*(block_diagonal F,d)*>)) by Def5;
then A12: len (block_diagonal (<*M*> ^ <*(block_diagonal F,d)*>),d) = (len M) + (len (block_diagonal F,d)) by A11, A9, A3, RVSUM_1:105;
A13: Width (<*M*> ^ <*(block_diagonal F,d)*>) = (Width <*M*>) ^ (Width <*(block_diagonal F,d)*>) by Th18;
A14: Width (<*(block_diagonal F,d)*> ^ <*M*>) = (Width <*(block_diagonal F,d)*>) ^ (Width <*M*>) by Th18;
A15: Sum (Width <*M*>) = width M by Lm5;
A16: Sum (Width <*(block_diagonal F,d)*>) = width (block_diagonal F,d) by Lm5;
width (block_diagonal (<*(block_diagonal F,d)*> ^ <*M*>),d) = Sum (Width (<*(block_diagonal F,d)*> ^ <*M*>)) by Def5;
then A17: width (block_diagonal (<*(block_diagonal F,d)*> ^ <*M*>),d) = (width (block_diagonal F,d)) + (width M) by A14, A15, A16, RVSUM_1:105;
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 A5, A7, A10, A17, Th32 ; :: 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 A5, A1, A13, A16, A12, A6, A8, FINSEQ_1:4, RVSUM_1:105, B9
.= block_diagonal F,d by Th33 ; :: thesis: verum