let K be Field; :: thesis: for A1, B1, A2, B2 being Matrix of K st width A1 = len B1 & width A2 = len B2 holds
(block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K)) = block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)
let A1, B1, A2, B2 be Matrix of K; :: thesis: ( width A1 = len B1 & width A2 = len B2 implies (block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K)) = block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K) )
assume that
A1: width A1 = len B1 and
A2: width A2 = len B2 ; :: thesis: (block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K)) = block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)
set a1 = <*A1*>;
set a2 = <*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*>,(0. K);
set bB = block_diagonal <*B1,B2*>,(0. K);
set bAB = block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K);
A3: ( Width <*A1,A2*> = (Width <*A1*>) ^ (Width <*A2*>) & Len <*B1,B2*> = (Len <*B1*>) ^ (Len <*B2*>) & Width <*A1*> = <*(width A1)*> & Width <*A2*> = <*(width A2)*> & Len <*B1*> = <*(len B1)*> & Len <*B2*> = <*(len B2)*> & Sum (Len <*A1,A2*>) = len (block_diagonal <*A1,A2*>,(0. K)) & Sum (Width <*A1,A2*>) = width (block_diagonal <*A1,A2*>,(0. K)) & Sum (Len <*B1,B2*>) = len (block_diagonal <*B1,B2*>,(0. K)) & Sum (Width <*B1,B2*>) = width (block_diagonal <*B1,B2*>,(0. K)) & Sum (Len (<*A1,A2*> (#) <*B1,B2*>)) = len (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) & Sum (Width (<*A1,A2*> (#) <*B1,B2*>)) = width (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) ) by Th14, Th15, Th18, Th19, Def5;
then A4: ( len ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) = Sum (Len <*A1,A2*>) & width ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) = Sum (Width <*B1,B2*>) & Len (<*A1,A2*> (#) <*B1,B2*>) = Len <*A1,A2*> & Width (<*A1,A2*> (#) <*B1,B2*>) = Width <*B1,B2*> & Sum (Len <*A1,A2*>) = (len A1) + (len A2) & Sum (Width <*B1,B2*>) = (width B1) + (width B2) ) by A1, A2, Th73, Th16, Th20, MATRIX_3:def 4;
set bAbB = (block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K));
A5: <*A1,A2*> (#) <*B1,B2*> = <*(A1 * B1),(A2 * B2)*> by Th77;
A6: ( width (A1 * B1) = width B1 & len (A1 * B1) = len A1 & width (A2 * B2) = width B2 & len (A2 * B2) = len A2 ) by A1, A2, MATRIX_3:def 4;
A7: Indices (A1 * B1) = [:(Seg (len (A1 * B1))),(Seg (width (A1 * B1))):] by FINSEQ_1:def 3
.= [:(dom A1),(Seg (width B1)):] by A6, FINSEQ_1:def 3 ;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) implies (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j = ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j )
assume A8: [i,j] in Indices (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) ; :: thesis: (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j = ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j
Indices (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) = [:(Seg (len (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)))),(Seg (width (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)))):] by FINSEQ_1:def 3
.= Indices ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) by A3, A4, FINSEQ_1:def 3 ;
then A9: ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (Line (block_diagonal <*A1,A2*>,(0. K)),i) "*" (Col (block_diagonal <*B1,B2*>,(0. K)),j) by A1, A2, A3, A8, MATRIX_3:def 4
.= Sum (mlt (Line (block_diagonal <*A1,A2*>,(0. K)),i),(Col (block_diagonal <*B1,B2*>,(0. K)),j)) ;
A10: ( i in dom (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) & j in Seg (width (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K))) & dom (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) = Seg (len (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K))) ) by A8, FINSEQ_1:def 3, ZFMISC_1:106;
then A11: ( 1 <= i & 1 <= j ) by FINSEQ_1:3;

now

per cases ( i <= len A1 or i > len A1 ) ;

suppose i <= len A1 ; :: thesis: ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j

then A12: ( i in dom A1 & i in dom (A1 * B1) ) by A6, A11, FINSEQ_3:27;
then A13: Line (block_diagonal <*A1,A2*>,(0. K)),i = (Line A1,i) ^ ((width A2) |-> (0. K)) by Th23;

now

per cases ( j <= width B1 or j > width B1 ) ;

suppose j <= width B1 ; :: thesis: ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j

then A14: ( j in Seg (width B1) & dom (Line (A1 * B1),i) = Seg (width B1) ) by A6, A11, FINSEQ_1:3, FINSEQ_2:144;
then A15: ( Col (block_diagonal <*B1,B2*>,(0. K)),j = (Col B1,j) ^ ((len B2) |-> (0. K)) & [i,j] in Indices (A1 * B1) ) by A7, A12, Th24, ZFMISC_1:106;
hence ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (Sum (mlt (Line A1,i),(Col B1,j))) + (Sum (mlt ((width A2) |-> (0. K)),((len B2) |-> (0. K)))) by A1, A2, A9, A13, Lm9
.= (Sum (mlt (Line A1,i),(Col B1,j))) + (Sum ((0. K) * ((width A2) |-> (0. K)))) by A2, FVSUM_1:80
.= (Sum (mlt (Line A1,i),(Col B1,j))) + ((0. K) * (Sum ((width A2) |-> (0. K)))) by FVSUM_1:92
.= (Sum (mlt (Line A1,i),(Col B1,j))) + (0. K) by VECTSP_1:36
.= (Line A1,i) "*" (Col B1,j) by RLVECT_1:def 7
.= (A1 * B1) * i,j by A1, A15, MATRIX_3:def 4
.= (Line (A1 * B1),i) . j by A6, A14, MATRIX_1:def 8
.= ((Line (A1 * B1),i) ^ ((width (A2 * B2)) |-> (0. K))) . j by A14, FINSEQ_1:def 7
.= (Line (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)),i) . j by A5, A12, Th23
.= (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j by A10, MATRIX_1:def 8 ;
:: thesis: verum

end;

suppose A16: j > width B1 ; :: thesis: ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j

then reconsider J = j - (width B1) as Element of NAT by NAT_1:21;
A17: j = J + (width B1) ;
J <> 0 by A16;
then J > 0 ;
then A18: J in Seg (width B2) by A17, A10, A3, A4, FINSEQ_1:82;
then A19: ( Col (block_diagonal <*B1,B2*>,(0. K)),(J + (width B1)) = ((len B1) |-> (0. K)) ^ (Col B2,J) & len (Line (A1 * B1),i) = width B1 & dom ((width (A2 * B2)) |-> (0. K)) = Seg (width B2) ) by A6, Th24, FINSEQ_1:def 18, FINSEQ_2:144;
hence ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (Sum (mlt (Line A1,i),((len B1) |-> (0. K)))) + (Sum (mlt ((width A2) |-> (0. K)),(Col B2,J))) by A1, A2, A9, A13, Lm9
.= (Sum (mlt (Line A1,i),((len B1) |-> (0. K)))) + (Sum ((0. K) * (Col B2,J))) by A2, FVSUM_1:80
.= (Sum ((0. K) * (Line A1,i))) + (Sum ((0. K) * (Col B2,J))) by A1, FVSUM_1:80
.= (Sum ((0. K) * (Line A1,i))) + ((0. K) * (Sum (Col B2,J))) by FVSUM_1:92
.= ((0. K) * (Sum (Line A1,i))) + ((0. K) * (Sum (Col B2,J))) by FVSUM_1:92
.= ((0. K) * (Sum (Line A1,i))) + (0. K) by VECTSP_1:36
.= (0. K) + (0. K) by VECTSP_1:36
.= 0. K by RLVECT_1:def 7
.= ((width (A2 * B2)) |-> (0. K)) . J by A6, A18, FINSEQ_2:71
.= ((Line (A1 * B1),i) ^ ((width (A2 * B2)) |-> (0. K))) . (J + (width (A1 * B1))) by A6, A18, A19, FINSEQ_1:def 7
.= (Line (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)),i) . j by A5, A12, Th23, A6
.= (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j by A10, MATRIX_1:def 8 ;
:: thesis: verum

end;

end;

end;

hence ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j ; :: thesis: verum

end;

suppose A20: i > len A1 ; :: thesis: ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j

then reconsider I = i - (len A1) as Element of NAT by NAT_1:21;
A21: i = I + (len A1) ;
I <> 0 by A20;
then I > 0 ;
then I in Seg (len A2) by A21, A10, A3, A4, FINSEQ_1:82;
then A22: ( I in dom A2 & dom A2 = dom (A2 * B2) ) by A6, FINSEQ_1:def 3, FINSEQ_3:31;
then A23: Line (block_diagonal <*A1,A2*>,(0. K)),(I + (len A1)) = ((width A1) |-> (0. K)) ^ (Line A2,I) by Th23;

now

per cases ( j <= width B1 or j > width B1 ) ;

suppose j <= width B1 ; :: thesis: ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j

then A24: ( j in Seg (width B1) & dom ((width (A1 * B1)) |-> (0. K)) = Seg (width B1) ) by A6, A11, FINSEQ_1:3, FINSEQ_2:144;
then Col (block_diagonal <*B1,B2*>,(0. K)),j = (Col B1,j) ^ ((len B2) |-> (0. K)) by Th24;
hence ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (Sum (mlt ((width A1) |-> (0. K)),(Col B1,j))) + (Sum (mlt (Line A2,I),((len B2) |-> (0. K)))) by A1, A2, A9, A23, Lm9
.= (Sum (mlt ((width A1) |-> (0. K)),(Col B1,j))) + (Sum ((0. K) * (Line A2,I))) by A2, FVSUM_1:80
.= (Sum ((0. K) * (Col B1,j))) + (Sum ((0. K) * (Line A2,I))) by A1, FVSUM_1:80
.= (Sum ((0. K) * (Col B1,j))) + ((0. K) * (Sum (Line A2,I))) by FVSUM_1:92
.= ((0. K) * (Sum (Col B1,j))) + ((0. K) * (Sum (Line A2,I))) by FVSUM_1:92
.= ((0. K) * (Sum (Col B1,j))) + (0. K) by VECTSP_1:36
.= (0. K) + (0. K) by VECTSP_1:36
.= 0. K by RLVECT_1:def 7
.= ((width (A1 * B1)) |-> (0. K)) . j by A6, A24, FINSEQ_2:71
.= (((width (A1 * B1)) |-> (0. K)) ^ (Line (A2 * B2),I)) . j by A24, FINSEQ_1:def 7
.= (Line (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)),(I + (len A1))) . j by A6, A5, A22, Th23
.= (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j by A10, MATRIX_1:def 8 ;
:: thesis: verum

end;

suppose A25: j > width B1 ; :: thesis: ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j

then reconsider J = j - (width B1) as Element of NAT by NAT_1:21;
A26: j = J + (width B1) ;
J <> 0 by A25;
then J > 0 ;
then A27: ( J in Seg (width B2) & dom (Line (A2 * B2),I) = Seg (width B2) & len ((width (A1 * B1)) |-> (0. K)) = width B1 ) by A6, A26, A10, A3, A4, FINSEQ_1:82, FINSEQ_1:def 18, FINSEQ_2:144;
then A28: ( Col (block_diagonal <*B1,B2*>,(0. K)),(J + (width B1)) = ((len B1) |-> (0. K)) ^ (Col B2,J) & [I,J] in Indices (A2 * B2) ) by A22, A6, Th24, ZFMISC_1:106;
hence ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (Sum (mlt ((width A1) |-> (0. K)),((len B1) |-> (0. K)))) + (Sum (mlt (Line A2,I),(Col B2,J))) by A1, A2, A9, A23, Lm9
.= (Sum ((0. K) * ((width A1) |-> (0. K)))) + (Sum (mlt (Line A2,I),(Col B2,J))) by A1, FVSUM_1:80
.= ((0. K) * (Sum ((width A1) |-> (0. K)))) + (Sum (mlt (Line A2,I),(Col B2,J))) by FVSUM_1:92
.= (0. K) + (Sum (mlt (Line A2,I),(Col B2,J))) by VECTSP_1:36
.= (Line A2,I) "*" (Col B2,J) by RLVECT_1:def 7
.= (A2 * B2) * I,J by A28, A2, MATRIX_3:def 4
.= (Line (A2 * B2),I) . J by A27, A6, MATRIX_1:def 8
.= (((width (A1 * B1)) |-> (0. K)) ^ (Line (A2 * B2),I)) . (J + (width B1)) by A27, FINSEQ_1:def 7
.= (Line (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)),(I + (len A1))) . j by A6, A5, A22, Th23
.= (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j by A10, MATRIX_1:def 8 ;
:: thesis: verum

end;

end;

end;

hence ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j ; :: thesis: verum

end;

end;

end;

hence (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j = ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j ; :: thesis: verum

end;

hence (block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K)) = block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K) by A3, A4, MATRIX_1:21; :: thesis: verum