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 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; 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; 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; ( 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 = {}
; ( 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:27, MATRIX_0:def 3;
then A8:
Sum (Width <*M*>) = 0
by Lm5;
A9:
Sum (Len <*M*>) = len M
by Lm4;
A10:
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 A11:
len (block_diagonal ((<*(block_diagonal (F,d))*> ^ <*M*>),d)) = (len (block_diagonal (F,d))) + (len M)
by A2, A9, A3, RVSUM_1:75;
A12:
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 A13:
len (block_diagonal ((<*M*> ^ <*(block_diagonal (F,d))*>),d)) = (len M) + (len (block_diagonal (F,d)))
by A12, A9, A3, RVSUM_1:75;
A14:
Width (<*M*> ^ <*(block_diagonal (F,d))*>) = (Width <*M*>) ^ (Width <*(block_diagonal (F,d))*>)
by Th18;
A15:
Width (<*(block_diagonal (F,d))*> ^ <*M*>) = (Width <*(block_diagonal (F,d))*>) ^ (Width <*M*>)
by Th18;
A16:
Sum (Width <*M*>) = width M
by Lm5;
A17:
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 A18:
width (block_diagonal ((<*(block_diagonal (F,d))*> ^ <*M*>),d)) = (width (block_diagonal (F,d))) + (width M)
by A15, A16, A17, RVSUM_1:75;
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, A11, A18, Th32
; 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, A14, A17, A13, A6, A8, A10, RVSUM_1:75
.=
block_diagonal (F,d)
by Th33
; verum