let K be Field; :: thesis: for a1, a2 being Element of K
for A1, B1, A2, 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, B1, A2, 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, B1, A2, 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_2:7;
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

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, FINSEQ_1:3;
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_2:10;
A23: bAbB . i = Line ((block_diagonal <*A1,A2*>,a1) + (block_diagonal <*B1,B2*>,a2)),i by A16, A7, A11, A21, MATRIX_2:10;
A24: dom (A1 ^ A2) = Seg (len (block_diagonal (<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) by A8, A16, A11, FINSEQ_1:def 7;

now

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:38;

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 FINSEQ_1:def 18;
A27: dom A1 = dom B1 by A1, FINSEQ_3:31;
A28: len (Line A1,i) = width A1 by FINSEQ_1:def 18;
dom A1 = dom (A1 + B1) by A6, FINSEQ_3:31;
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:25
.= ((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 FINSEQ_1:def 18;
A31: dom A2 = dom B2 by A2, FINSEQ_3:31;
A32: len ((width (A1 + B1)) |-> a2) = width (A1 + B1) by FINSEQ_1:def 18;
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:31;
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:25
.= (((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, FINSEQ_1:18; :: thesis: verum
set b2 = <*B2*>;
set b1 = <*B1*>;
set d2 = <*A2*>;
set d1 = <*A1*>;