let K be Field; :: thesis: for a1, a2 being Element of K
for A1, A2, B1, B2 being Matrix of K st len A1 = len B1 & len A2 = len B2 & width A1 = width B1 & width A2 = width B2 holds
(block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2)) = block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))
let a1, a2 be Element of K; :: thesis: for A1, A2, B1, B2 being Matrix of K st len A1 = len B1 & len A2 = len B2 & width A1 = width B1 & width A2 = width B2 holds
(block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2)) = block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))
let A1, A2, B1, B2 be Matrix of K; :: thesis: ( len A1 = len B1 & len A2 = len B2 & width A1 = width B1 & width A2 = width B2 implies (block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2)) = block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2)) )
assume that
A1: len A1 = len B1 and
A2: len A2 = len B2 and
A3: width A1 = width B1 and
A4: width A2 = width B2 ; :: thesis: (block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2)) = block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))
set b12 = <*B1,B2*>;
set a12 = <*A1,A2*>;
set AB2 = A2 + B2;
set AB1 = A1 + B1;
set ab = <*A1,A2*> (+) <*B1,B2*>;
set bA = block_diagonal (<*A1,A2*>,a1);
set bB = block_diagonal (<*B1,B2*>,a2);
set bAB = block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2));
A5: len ((block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2))) = len (block_diagonal (<*A1,A2*>,a1)) by MATRIX_3:def 3;
width ((block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2))) = width (block_diagonal (<*A1,A2*>,a1)) by MATRIX_3:def 3;
then reconsider bAbB = (block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2)) as Matrix of len (block_diagonal (<*A1,A2*>,a1)), width (block_diagonal (<*A1,A2*>,a1)),K by A5, MATRIX_0:51;
A6: len (A1 + B1) = len A1 by MATRIX_3:def 3;
A7: len (block_diagonal (<*A1,A2*>,a1)) = Sum (Len <*A1,A2*>) by Def5;
A8: Sum (Len <*A1,A2*>) = (len A1) + (len A2) by Th16;
A9: len (A2 + B2) = len A2 by MATRIX_3:def 3;
A10: Sum (Width <*B1,B2*>) = (width B1) + (width B2) by Th20;
A11: len (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) = Sum (Len (<*A1,A2*> (+) <*B1,B2*>)) by Def5;
A12: width (block_diagonal (<*B1,B2*>,a2)) = Sum (Width <*B1,B2*>) by Def5;
A13: width (block_diagonal (<*A1,A2*>,a1)) = Sum (Width <*A1,A2*>) by Def5;
A14: width (A2 + B2) = width A2 by MATRIX_3:def 3;
A15: width (A1 + B1) = width A1 by MATRIX_3:def 3;
A16: Len (<*A1,A2*> (+) <*B1,B2*>) = Len <*A1,A2*> by Th66;
A17: <*A1,A2*> (+) <*B1,B2*> = <*(A1 + B1),(A2 + B2)*> by Th70;

now :: thesis: for i being Nat st 1 <= i & i <= len (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) holds
(block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = ((block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2))) . i

A18: dom (block_diagonal (<*A1,A2*>,a1)) = Seg (len (block_diagonal (<*A1,A2*>,a1))) by FINSEQ_1:def 3;
let i be Nat; :: thesis: ( 1 <= i & i <= len (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) implies (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = ((block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2))) . i )
assume that
A19: 1 <= i and
A20: i <= len (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) ; :: thesis: (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = ((block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2))) . i
A21: i in Seg (len (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2)))) by A19, A20;
then A22: (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = Line ((block_diagonal (<*(A1 + B1),(A2 + B2)*>,(a1 + a2))),i) by A17, A11, MATRIX_0:52;
A23: bAbB . i = Line (((block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2))),i) by A16, A7, A11, A21, MATRIX_0:52;
A24: dom (A1 ^ A2) = Seg (len (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2)))) by A8, A16, A11, FINSEQ_1:def 7;

now :: thesis: (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = bAbB . i

per cases ( i in dom A1 or ex n being Nat st
( n in dom A2 & i = (len A1) + n ) ) by A21, A24, FINSEQ_1:25;

suppose A25: i in dom A1 ; :: thesis: (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = bAbB . i

A26: len (Line (B1,i)) = width B1 by CARD_1:def 7;
A27: dom A1 = dom B1 by A1, FINSEQ_3:29;
A28: len (Line (A1,i)) = width A1 by CARD_1:def 7;
dom A1 = dom (A1 + B1) by A6, FINSEQ_3:29;
hence (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = (Line ((A1 + B1),i)) ^ ((width (A2 + B2)) |-> (a1 + a2)) by A22, A25, Th23
.= ((Line (A1,i)) + (Line (B1,i))) ^ ((width (A2 + B2)) |-> (a1 + a2)) by A3, A25, Lm8
.= ((Line (A1,i)) + (Line (B1,i))) ^ (((width (A2 + B2)) |-> a1) + ((width (A2 + B2)) |-> a2)) by FVSUM_1:20
.= ((Line (A1,i)) ^ ((width A2) |-> a1)) + ((Line (B1,i)) ^ ((width B2) |-> a2)) by A3, A4, A14, A28, A26, Th1
.= (Line ((block_diagonal (<*A1,A2*>,a1)),i)) + ((Line (B1,i)) ^ ((width B2) |-> a2)) by A25, Th23
.= (Line ((block_diagonal (<*A1,A2*>,a1)),i)) + (Line ((block_diagonal (<*B1,B2*>,a2)),i)) by A25, A27, Th23
.= bAbB . i by A3, A4, A10, A16, A7, A13, A12, A11, A21, A18, A23, Lm8, Th20 ;
:: thesis: verum

end;

suppose A29: ex n being Nat st
( n in dom A2 & i = (len A1) + n ) ; :: thesis: (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = bAbB . i

A30: len ((width (A1 + B1)) |-> a1) = width (A1 + B1) by CARD_1:def 7;
A31: dom A2 = dom B2 by A2, FINSEQ_3:29;
A32: len ((width (A1 + B1)) |-> a2) = width (A1 + B1) by CARD_1:def 7;
consider n being Nat such that
A33: n in dom A2 and
A34: i = (len A1) + n by A29;
dom A2 = dom (A2 + B2) by A9, FINSEQ_3:29;
hence (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = ((width (A1 + B1)) |-> (a1 + a2)) ^ (Line ((A2 + B2),n)) by A6, A22, A33, A34, Th23
.= ((width (A1 + B1)) |-> (a1 + a2)) ^ ((Line (A2,n)) + (Line (B2,n))) by A4, A33, Lm8
.= (((width (A1 + B1)) |-> a1) + ((width (A1 + B1)) |-> a2)) ^ ((Line (A2,n)) + (Line (B2,n))) by FVSUM_1:20
.= (((width (A1 + B1)) |-> a1) ^ (Line (A2,n))) + (((width (A1 + B1)) |-> a2) ^ (Line (B2,n))) by A30, A32, Th1
.= (Line ((block_diagonal (<*A1,A2*>,a1)),i)) + (((width B1) |-> a2) ^ (Line (B2,n))) by A3, A15, A33, A34, Th23
.= (Line ((block_diagonal (<*A1,A2*>,a1)),i)) + (Line ((block_diagonal (<*B1,B2*>,a2)),i)) by A1, A33, A34, A31, Th23
.= bAbB . i by A3, A4, A10, A16, A7, A13, A12, A11, A21, A18, A23, Lm8, Th20 ;
:: thesis: verum

end;

end;

end;

hence (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = ((block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2))) . i ; :: thesis: verum

end;

hence (block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2)) = block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2)) by A16, A7, A11, A5; :: thesis: verum