let K be Field; :: thesis: for a1, a2, b1, b2, c1, c2, d1, d2 being Element of K holds (a1,b1 ][ c1,d1) * (a2,b2 ][ c2,d2) = ((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2)) ][ ((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2))
let a1, a2, b1, b2, c1, c2, d1, d2 be Element of K; :: thesis: (a1,b1 ][ c1,d1) * (a2,b2 ][ c2,d2) = ((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2)) ][ ((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2))
reconsider A = a1,b1 ][ c1,d1 as Matrix of 2,K ;
reconsider B = a2,b2 ][ c2,d2 as Matrix of 2,K ;
reconsider D = ((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2)) ][ ((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2)) as Matrix of 2,K ;
A1: width A = 2 by MATRIX_1:25;
2 in {1,2} by TARSKI:def 2;
then A2: (Line A,2) . 2 = A * 2,2 by A1, FINSEQ_1:4, MATRIX_1:def 8
.= d1 by MATRIX_2:6 ;
A3: len (Line A,2) = width A by MATRIX_1:def 8
.= 2 by MATRIX_1:25 ;
1 in {1,2} by TARSKI:def 2;
then (Line A,2) . 1 = A * 2,1 by A1, FINSEQ_1:4, MATRIX_1:def 8
.= c1 by MATRIX_2:6 ;
then A4: Line A,2 = <*c1,d1*> by A3, A2, FINSEQ_1:61;
2 in {1,2} by TARSKI:def 2;
then A5: (Line A,1) . 2 = A * 1,2 by A1, FINSEQ_1:4, MATRIX_1:def 8
.= b1 by MATRIX_2:6 ;
A6: len (Line A,1) = width A by MATRIX_1:def 8
.= 2 by MATRIX_1:25 ;
1 in {1,2} by TARSKI:def 2;
then (Line A,1) . 1 = A * 1,1 by A1, FINSEQ_1:4, MATRIX_1:def 8
.= a1 by MATRIX_2:6 ;
then A7: Line A,1 = <*a1,b1*> by A6, A5, FINSEQ_1:61;
A8: len (Col B,2) = len B by MATRIX_1:def 9
.= 2 by MATRIX_1:25 ;
A9: len (Col B,1) = len B by MATRIX_1:def 9
.= 2 by MATRIX_1:25 ;
reconsider C = A * B as Matrix of K ;
A10: len B = 2 by MATRIX_1:25;
width B = 2 by MATRIX_1:25;
then A11: width C = 2 by A1, A10, Def4;
len A = 2 by MATRIX_1:25;
then A12: len C = 2 by A1, A10, Def4;
then reconsider C = C as Matrix of 2,K by A11, MATRIX_2:7;
A13: Seg (len B) = dom B by FINSEQ_1:def 3;
2 in {1,2} by TARSKI:def 2;
then A14: (Col B,2) . 2 = B * 2,2 by A10, A13, FINSEQ_1:4, MATRIX_1:def 9
.= d2 by MATRIX_2:6 ;
1 in {1,2} by TARSKI:def 2;
then (Col B,2) . 1 = B * 1,2 by A10, A13, FINSEQ_1:4, MATRIX_1:def 9
.= b2 by MATRIX_2:6 ;
then A15: Col B,2 = <*b2,d2*> by A8, A14, FINSEQ_1:61;
2 in {1,2} by TARSKI:def 2;
then A16: (Col B,1) . 2 = B * 2,1 by A10, A13, FINSEQ_1:4, MATRIX_1:def 9
.= c2 by MATRIX_2:6 ;
1 in {1,2} by TARSKI:def 2;
then (Col B,1) . 1 = B * 1,1 by A10, A13, FINSEQ_1:4, MATRIX_1:def 9
.= a2 by MATRIX_2:6 ;
then A17: Col B,1 = <*a2,c2*> by A9, A16, FINSEQ_1:61;
dom C = Seg (len C) by FINSEQ_1:def 3;
then A18: Indices C = [:(Seg 2),(Seg 2):] by A12, A11, MATRIX_1:def 5;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices C implies C * i,j = D * i,j )
assume A19: [i,j] in Indices C ; :: thesis: C * i,j = D * i,j
then A20: ( i in Seg 2 & j in Seg 2 ) by A18, ZFMISC_1:106;

now

per cases ( ( i = 1 & j = 1 ) or ( i = 1 & j = 2 ) or ( i = 2 & j = 1 ) or ( i = 2 & j = 2 ) ) by A20, FINSEQ_1:4, TARSKI:def 2;

case ( i = 1 & j = 1 ) ; :: thesis: C * 1,1 = D * 1,1

hence C * 1,1 = <*a1,b1*> "*" <*a2,c2*> by A1, A10, A7, A17, A19, Def4
.= (a1 * a2) + (b1 * c2) by FVSUM_1:114
.= D * 1,1 by MATRIX_2:6 ;
:: thesis: verum

end;

case ( i = 1 & j = 2 ) ; :: thesis: C * 1,2 = D * 1,2

hence C * 1,2 = <*a1,b1*> "*" <*b2,d2*> by A1, A10, A7, A15, A19, Def4
.= (a1 * b2) + (b1 * d2) by FVSUM_1:114
.= D * 1,2 by MATRIX_2:6 ;
:: thesis: verum

end;

case ( i = 2 & j = 1 ) ; :: thesis: C * 2,1 = D * 2,1

hence C * 2,1 = <*c1,d1*> "*" <*a2,c2*> by A1, A10, A4, A17, A19, Def4
.= (c1 * a2) + (d1 * c2) by FVSUM_1:114
.= D * 2,1 by MATRIX_2:6 ;
:: thesis: verum

end;

case ( i = 2 & j = 2 ) ; :: thesis: C * 2,2 = D * 2,2

hence C * 2,2 = <*c1,d1*> "*" <*b2,d2*> by A1, A10, A4, A15, A19, Def4
.= (c1 * b2) + (d1 * d2) by FVSUM_1:114
.= D * 2,2 by MATRIX_2:6 ;
:: thesis: verum

end;

end;

end;

hence C * i,j = D * i,j ; :: thesis: verum

end;

hence (a1,b1 ][ c1,d1) * (a2,b2 ][ c2,d2) = ((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2)) ][ ((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2)) by MATRIX_1:28; :: thesis: verum