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 & len A2 = len B2 ) and
A2: ( width A1 = width B1 & width A2 = width B2 ) ; :: thesis: (block_diagonal <*A1,A2*>,a1) + (block_diagonal <*B1,B2*>,a2) = block_diagonal (<*A1,A2*> (+) <*B1,B2*>),(a1 + a2)
set AB1 = A1 + B1;
set AB2 = A2 + B2;
set d1 = <*A1*>;
set d2 = <*A2*>;
set b1 = <*B1*>;
set b2 = <*B2*>;
set a12 = <*A1,A2*>;
set b12 = <*B1,B2*>;
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);
A3: <*A1,A2*> (+) <*B1,B2*> = <*(A1 + B1),(A2 + B2)*> by Th70;
A4: ( Sum (Width <*A1,A2*>) = (width A1) + (width A2) & Sum (Len <*A1,A2*>) = (len A1) + (len A2) & Sum (Width <*B1,B2*>) = (width B1) + (width B2) & Sum (Len <*B1,B2*>) = (len B1) + (len B2) ) by Th16, Th20;
A5: ( Len (<*A1,A2*> (+) <*B1,B2*>) = Len <*A1,A2*> & len (block_diagonal <*A1,A2*>,a1) = Sum (Len <*A1,A2*>) & width (block_diagonal <*A1,A2*>,a1) = Sum (Width <*A1,A2*>) & len (block_diagonal <*B1,B2*>,a2) = Sum (Len <*B1,B2*>) & width (block_diagonal <*B1,B2*>,a2) = Sum (Width <*B1,B2*>) ) by Th66, Def5;
A6: ( len (block_diagonal (<*A1,A2*> (+) <*B1,B2*>),(a1 + a2)) = Sum (Len (<*A1,A2*> (+) <*B1,B2*>)) & len ((block_diagonal <*A1,A2*>,a1) + (block_diagonal <*B1,B2*>,a2)) = len (block_diagonal <*A1,A2*>,a1) & width ((block_diagonal <*A1,A2*>,a1) + (block_diagonal <*B1,B2*>,a2)) = width (block_diagonal <*A1,A2*>,a1) ) by Def5, MATRIX_3:def 3;
A7: ( len (A1 + B1) = len A1 & len (A2 + B2) = len A2 & width (A1 + B1) = width A1 & width (A2 + B2) = width A2 ) by MATRIX_3:def 3;
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 A6, MATRIX_2:7;

now

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 A8: ( 1 <= i & 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
A9: ( i in Seg (len (block_diagonal (<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) & dom (A1 ^ A2) = Seg (len (block_diagonal (<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) & dom (block_diagonal <*A1,A2*>,a1) = Seg (len (block_diagonal <*A1,A2*>,a1)) ) by A8, A4, A5, A6, FINSEQ_1:3, FINSEQ_1:def 3, FINSEQ_1:def 7;
then A10: ( (block_diagonal (<*A1,A2*> (+) <*B1,B2*>),(a1 + a2)) . i = Line (block_diagonal <*(A1 + B1),(A2 + B2)*>,(a1 + a2)),i & bAbB . i = Line ((block_diagonal <*A1,A2*>,a1) + (block_diagonal <*B1,B2*>,a2)),i ) by A3, A5, A6, MATRIX_2:10;

now

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

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

A12: ( len (Line A1,i) = width A1 & len (Line B1,i) = width B1 ) by FINSEQ_1:def 18;
A13: ( dom A1 = dom (A1 + B1) & dom A1 = dom B1 ) by A1, A7, FINSEQ_3:31;
hence (block_diagonal (<*A1,A2*> (+) <*B1,B2*>),(a1 + a2)) . i = (Line (A1 + B1),i) ^ ((width (A2 + B2)) |-> (a1 + a2)) by A10, A11, Th23
.= ((Line A1,i) + (Line B1,i)) ^ ((width (A2 + B2)) |-> (a1 + a2)) by A11, A1, A2, 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 A2, A7, A12, Th1
.= (Line (block_diagonal <*A1,A2*>,a1),i) + ((Line B1,i) ^ ((width B2) |-> a2)) by A11, Th23
.= (Line (block_diagonal <*A1,A2*>,a1),i) + (Line (block_diagonal <*B1,B2*>,a2),i) by A11, A13, Th23
.= bAbB . i by A9, A10, A1, A2, A4, A5, A6, Lm8 ;
:: thesis: verum

end;

suppose 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

then consider n being Nat such that
A14: ( n in dom A2 & i = (len A1) + n ) ;
A15: ( len ((width (A1 + B1)) |-> a1) = width (A1 + B1) & len ((width (A1 + B1)) |-> a2) = width (A1 + B1) ) by FINSEQ_1:def 18;
A16: ( dom A2 = dom (A2 + B2) & dom A2 = dom B2 ) by A1, A7, FINSEQ_3:31;
hence (block_diagonal (<*A1,A2*> (+) <*B1,B2*>),(a1 + a2)) . i = ((width (A1 + B1)) |-> (a1 + a2)) ^ (Line (A2 + B2),n) by A10, A14, Th23, A7
.= ((width (A1 + B1)) |-> (a1 + a2)) ^ ((Line A2,n) + (Line B2,n)) by A14, A1, A2, 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 A15, Th1
.= (Line (block_diagonal <*A1,A2*>,a1),i) + (((width B1) |-> a2) ^ (Line B2,n)) by A2, A7, A14, Th23
.= (Line (block_diagonal <*A1,A2*>,a1),i) + (Line (block_diagonal <*B1,B2*>,a2),i) by A1, A14, A16, Th23
.= bAbB . i by A9, A10, A1, A2, A4, A5, A6, Lm8 ;
:: 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 A5, A6, FINSEQ_1:18; :: thesis: verum