let K be Field; :: thesis: for A1, A2, B1, 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, A2, B1, 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))
A3: width (A1 * B1) = width B1 by A1, MATRIX_3:def 4;
set b12 = <*B1,B2*>;
set a12 = <*A1,A2*>;
set b2 = <*B2*>;
set b1 = <*B1*>;
set a2 = <*A2*>;
set a1 = <*A1*>;
set ab = <*A1,A2*> (#) <*B1,B2*>;
A4: Len <*B1,B2*> = (Len <*B1*>) ^ (Len <*B2*>) by Th14;
set bB = block_diagonal (<*B1,B2*>,(0. K));
set bA = block_diagonal (<*A1,A2*>,(0. K));
A5: Sum (Width <*A1,A2*>) = width (block_diagonal (<*A1,A2*>,(0. K))) by Def5;
A6: Sum (Len <*B1,B2*>) = len (block_diagonal (<*B1,B2*>,(0. K))) by Def5;
A7: Width <*A1*> = <*(width A1)*> by Th19;
set bAbB = (block_diagonal (<*A1,A2*>,(0. K))) * (block_diagonal (<*B1,B2*>,(0. K)));
set bAB = block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K));
A8: Sum (Len (<*A1,A2*> (#) <*B1,B2*>)) = len (block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K))) by Def5;
A9: Sum (Width (<*A1,A2*> (#) <*B1,B2*>)) = width (block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K))) by Def5;
A10: Sum (Len <*A1,A2*>) = (len A1) + (len A2) by Th16;
A11: Sum (Width <*B1,B2*>) = (width B1) + (width B2) by Th20;
A12: len (A2 * B2) = len A2 by A2, MATRIX_3:def 4;
A13: <*A1,A2*> (#) <*B1,B2*> = <*(A1 * B1),(A2 * B2)*> by Th77;
A14: Width <*A2*> = <*(width A2)*> by Th19;
A15: Len <*B2*> = <*(len B2)*> by Th15;
A16: Len <*B1*> = <*(len B1)*> by Th15;
A17: Width <*A1,A2*> = (Width <*A1*>) ^ (Width <*A2*>) by Th18;
then A18: Len (<*A1,A2*> (#) <*B1,B2*>) = Len <*A1,A2*> by A1, A2, A4, A7, A14, A16, A15, Th73;
A19: Width (<*A1,A2*> (#) <*B1,B2*>) = Width <*B1,B2*> by A1, A2, A17, A4, A7, A14, A16, A15, Th73;
Sum (Len <*A1,A2*>) = len (block_diagonal (<*A1,A2*>,(0. K))) by Def5;
then A20: len ((block_diagonal (<*A1,A2*>,(0. K))) * (block_diagonal (<*B1,B2*>,(0. K)))) = Sum (Len <*A1,A2*>) by A1, A2, A17, A4, A7, A14, A16, A15, A5, A6, MATRIX_3:def 4;
A21: len (A1 * B1) = len A1 by A1, MATRIX_3:def 4;
Sum (Width <*B1,B2*>) = width (block_diagonal (<*B1,B2*>,(0. K))) by Def5;
then A22: width ((block_diagonal (<*A1,A2*>,(0. K))) * (block_diagonal (<*B1,B2*>,(0. K)))) = Sum (Width <*B1,B2*>) by A1, A2, A17, A4, A7, A14, A16, A15, A5, A6, MATRIX_3:def 4;
A23: width (A2 * B2) = width B2 by A2, MATRIX_3:def 4;
A24: Indices (A1 * B1) = [:(Seg (len (A1 * B1))),(Seg (width (A1 * B1))):] by FINSEQ_1:def 3
.= [:(dom A1),(Seg (width B1)):] by A3, A21, FINSEQ_1:def 3 ;

now :: thesis: for i, j being Nat st [i,j] in Indices (block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K))) holds
(block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K))) * (i,j) = ((block_diagonal (<*A1,A2*>,(0. K))) * (block_diagonal (<*B1,B2*>,(0. K)))) * (i,j)

A25: dom (block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K))) = Seg (len (block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K)))) by FINSEQ_1:def 3;
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 A26: [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)
A27: j in Seg (width (block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K)))) by A26, ZFMISC_1:87;
A28: i in dom (block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K))) by A26, ZFMISC_1:87;
then A29: 1 <= i by A25, FINSEQ_1:1;
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 A8, A9, A20, A22, A18, A19, FINSEQ_1:def 3 ;
then A30: ((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, A17, A4, A7, A14, A16, A15, A5, A6, A26, MATRIX_3:def 4
.= Sum (mlt ((Line ((block_diagonal (<*A1,A2*>,(0. K))),i)),(Col ((block_diagonal (<*B1,B2*>,(0. K))),j)))) ;
A31: 1 <= j by A27, FINSEQ_1:1;

now :: 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)

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

suppose A32: 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 A33: i in dom (A1 * B1) by A21, A29, FINSEQ_3:25;
A34: i in dom A1 by A29, A32, FINSEQ_3:25;
then A35: Line ((block_diagonal (<*A1,A2*>,(0. K))),i) = (Line (A1,i)) ^ ((width A2) |-> (0. K)) by Th23;

now :: 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)

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 A36: j in Seg (width B1) by A31;
then A37: [i,j] in Indices (A1 * B1) by A24, A34, ZFMISC_1:87;
A38: dom (Line ((A1 * B1),i)) = Seg (width B1) by A3, FINSEQ_2:124;
Col ((block_diagonal (<*B1,B2*>,(0. K))),j) = (Col (B1,j)) ^ ((len B2) |-> (0. K)) by A36, Th24;
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, A30, A35, Lm9
.= (Sum (mlt ((Line (A1,i)),(Col (B1,j))))) + (Sum ((0. K) * ((width A2) |-> (0. K)))) by A2, FVSUM_1:66
.= (Sum (mlt ((Line (A1,i)),(Col (B1,j))))) + ((0. K) * (Sum ((width A2) |-> (0. K)))) by FVSUM_1:73
.= (Sum (mlt ((Line (A1,i)),(Col (B1,j))))) + (0. K)
.= (Line (A1,i)) "*" (Col (B1,j)) by RLVECT_1:def 4
.= (A1 * B1) * (i,j) by A1, A37, MATRIX_3:def 4
.= (Line ((A1 * B1),i)) . j by A3, A36, MATRIX_0:def 7
.= ((Line ((A1 * B1),i)) ^ ((width (A2 * B2)) |-> (0. K))) . j by A36, A38, FINSEQ_1:def 7
.= (Line ((block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K))),i)) . j by A13, A33, Th23
.= (block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K))) * (i,j) by A27, MATRIX_0:def 7 ;
:: thesis: verum

end;

suppose A39: 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;
A40: j = J + (width B1) ;
A41: len (Line ((A1 * B1),i)) = width B1 by A3, CARD_1:def 7;
A42: dom ((width (A2 * B2)) |-> (0. K)) = Seg (width B2) by A23, FINSEQ_2:124;
J <> 0 by A39;
then A43: J in Seg (width B2) by A9, A19, A11, A27, A40, FINSEQ_1:61;
then Col ((block_diagonal (<*B1,B2*>,(0. K))),(J + (width B1))) = ((len B1) |-> (0. K)) ^ (Col (B2,J)) by Th24;
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, A30, A35, Lm9
.= (Sum (mlt ((Line (A1,i)),((len B1) |-> (0. K))))) + (Sum ((0. K) * (Col (B2,J)))) by A2, FVSUM_1:66
.= (Sum ((0. K) * (Line (A1,i)))) + (Sum ((0. K) * (Col (B2,J)))) by A1, FVSUM_1:66
.= (Sum ((0. K) * (Line (A1,i)))) + ((0. K) * (Sum (Col (B2,J)))) by FVSUM_1:73
.= ((0. K) * (Sum (Line (A1,i)))) + ((0. K) * (Sum (Col (B2,J)))) by FVSUM_1:73
.= ((0. K) * (Sum (Line (A1,i)))) + (0. K)
.= (0. K) + (0. K)
.= 0. K by RLVECT_1:def 4
.= ((width (A2 * B2)) |-> (0. K)) . J by A23, A43, FINSEQ_2:57
.= ((Line ((A1 * B1),i)) ^ ((width (A2 * B2)) |-> (0. K))) . (J + (width (A1 * B1))) by A3, A43, A41, A42, FINSEQ_1:def 7
.= (Line ((block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K))),i)) . j by A13, A3, A33, Th23
.= (block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K))) * (i,j) by A27, MATRIX_0:def 7 ;
:: 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 A44: 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;
A45: i = I + (len A1) ;
A46: dom A2 = dom (A2 * B2) by A12, FINSEQ_3:29;
I <> 0 by A44;
then I in Seg (len A2) by A8, A18, A10, A28, A25, A45, FINSEQ_1:61;
then A47: I in dom A2 by FINSEQ_1:def 3;
then A48: Line ((block_diagonal (<*A1,A2*>,(0. K))),(I + (len A1))) = ((width A1) |-> (0. K)) ^ (Line (A2,I)) by Th23;

now :: 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)

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

suppose A49: 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)

A50: dom ((width (A1 * B1)) |-> (0. K)) = Seg (width B1) by A3, FINSEQ_2:124;
A51: j in Seg (width B1) by A31, A49;
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, A30, A48, Lm9
.= (Sum (mlt (((width A1) |-> (0. K)),(Col (B1,j))))) + (Sum ((0. K) * (Line (A2,I)))) by A2, FVSUM_1:66
.= (Sum ((0. K) * (Col (B1,j)))) + (Sum ((0. K) * (Line (A2,I)))) by A1, FVSUM_1:66
.= (Sum ((0. K) * (Col (B1,j)))) + ((0. K) * (Sum (Line (A2,I)))) by FVSUM_1:73
.= ((0. K) * (Sum (Col (B1,j)))) + ((0. K) * (Sum (Line (A2,I)))) by FVSUM_1:73
.= ((0. K) * (Sum (Col (B1,j)))) + (0. K)
.= (0. K) + (0. K)
.= 0. K by RLVECT_1:def 4
.= ((width (A1 * B1)) |-> (0. K)) . j by A3, A51, FINSEQ_2:57
.= (((width (A1 * B1)) |-> (0. K)) ^ (Line ((A2 * B2),I))) . j by A51, A50, FINSEQ_1:def 7
.= (Line ((block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K))),(I + (len A1)))) . j by A13, A21, A47, A46, Th23
.= (block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K))) * (i,j) by A27, MATRIX_0:def 7 ;
:: thesis: verum

end;

suppose A52: 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;
A53: j = J + (width B1) ;
J <> 0 by A52;
then A54: J in Seg (width B2) by A9, A19, A11, A27, A53, FINSEQ_1:61;
then A55: [I,J] in Indices (A2 * B2) by A23, A47, A46, ZFMISC_1:87;
A56: len ((width (A1 * B1)) |-> (0. K)) = width B1 by A3, CARD_1:def 7;
A57: dom (Line ((A2 * B2),I)) = Seg (width B2) by A23, FINSEQ_2:124;
Col ((block_diagonal (<*B1,B2*>,(0. K))),(J + (width B1))) = ((len B1) |-> (0. K)) ^ (Col (B2,J)) by A54, Th24;
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, A30, A48, Lm9
.= (Sum ((0. K) * ((width A1) |-> (0. K)))) + (Sum (mlt ((Line (A2,I)),(Col (B2,J))))) by A1, FVSUM_1:66
.= ((0. K) * (Sum ((width A1) |-> (0. K)))) + (Sum (mlt ((Line (A2,I)),(Col (B2,J))))) by FVSUM_1:73
.= (0. K) + (Sum (mlt ((Line (A2,I)),(Col (B2,J)))))
.= (Line (A2,I)) "*" (Col (B2,J)) by RLVECT_1:def 4
.= (A2 * B2) * (I,J) by A2, A55, MATRIX_3:def 4
.= (Line ((A2 * B2),I)) . J by A23, A54, MATRIX_0:def 7
.= (((width (A1 * B1)) |-> (0. K)) ^ (Line ((A2 * B2),I))) . (J + (width B1)) by A54, A57, A56, FINSEQ_1:def 7
.= (Line ((block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K))),(I + (len A1)))) . j by A13, A21, A47, A46, Th23
.= (block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K))) * (i,j) by A27, MATRIX_0:def 7 ;
:: 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 A8, A9, A20, A22, A18, A19, MATRIX_0:21; :: thesis: verum