let K be Ring; :: 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_0:24;
2 in {1,2} by TARSKI:def 2;
then A2: (Line (A,2)) . 2 = A * (2,2) by A1, FINSEQ_1:2, MATRIX_0:def 7
.= d1 by MATRIX_0:50 ;
A3: len (Line (A,2)) = width A by MATRIX_0:def 7
.= 2 by MATRIX_0:24 ;
1 in {1,2} by TARSKI:def 2;
then (Line (A,2)) . 1 = A * (2,1) by A1, FINSEQ_1:2, MATRIX_0:def 7
.= c1 by MATRIX_0:50 ;
then A4: Line (A,2) = <*c1,d1*> by A3, A2, FINSEQ_1:44;
2 in {1,2} by TARSKI:def 2;
then A5: (Line (A,1)) . 2 = A * (1,2) by A1, FINSEQ_1:2, MATRIX_0:def 7
.= b1 by MATRIX_0:50 ;
A6: len (Line (A,1)) = width A by MATRIX_0:def 7
.= 2 by MATRIX_0:24 ;
1 in {1,2} by TARSKI:def 2;
then (Line (A,1)) . 1 = A * (1,1) by A1, FINSEQ_1:2, MATRIX_0:def 7
.= a1 by MATRIX_0:50 ;
then A7: Line (A,1) = <*a1,b1*> by A6, A5, FINSEQ_1:44;
A8: len (Col (B,2)) = len B by MATRIX_0:def 8
.= 2 by MATRIX_0:24 ;
A9: len (Col (B,1)) = len B by MATRIX_0:def 8
.= 2 by MATRIX_0:24 ;
reconsider C = A * B as Matrix of K ;
A10: len B = 2 by MATRIX_0:24;
width B = 2 by MATRIX_0:24;
then A11: width C = 2 by A1, A10, Def4;
len A = 2 by MATRIX_0:24;
then A12: len C = 2 by A1, A10, Def4;
then reconsider C = C as Matrix of 2,K by A11, MATRIX_0:51;
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:2, MATRIX_0:def 8
.= d2 by MATRIX_0:50 ;
1 in {1,2} by TARSKI:def 2;
then (Col (B,2)) . 1 = B * (1,2) by A10, A13, FINSEQ_1:2, MATRIX_0:def 8
.= b2 by MATRIX_0:50 ;
then A15: Col (B,2) = <*b2,d2*> by A8, A14, FINSEQ_1:44;
2 in {1,2} by TARSKI:def 2;
then A16: (Col (B,1)) . 2 = B * (2,1) by A10, A13, FINSEQ_1:2, MATRIX_0:def 8
.= c2 by MATRIX_0:50 ;
1 in {1,2} by TARSKI:def 2;
then (Col (B,1)) . 1 = B * (1,1) by A10, A13, FINSEQ_1:2, MATRIX_0:def 8
.= a2 by MATRIX_0:50 ;
then A17: Col (B,1) = <*a2,c2*> by A9, A16, FINSEQ_1:44;
dom C = Seg (len C) by FINSEQ_1:def 3;
then A18: Indices C = [:(Seg 2),(Seg 2):] by A12, A11;

now :: thesis: for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = D * (i,j)

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

now :: thesis: ( ( i = 1 & j = 1 & C * (1,1) = D * (1,1) ) or ( i = 1 & j = 2 & C * (1,2) = D * (1,2) ) or ( i = 2 & j = 1 & C * (2,1) = D * (2,1) ) or ( i = 2 & j = 2 & C * (2,2) = D * (2,2) ) )

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:2, 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:89
.= D * (1,1) by MATRIX_0:50 ;
:: 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:89
.= D * (1,2) by MATRIX_0:50 ;
:: 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:89
.= D * (2,1) by MATRIX_0:50 ;
:: 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:89
.= D * (2,2) by MATRIX_0:50 ;
:: 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_0:27; :: thesis: verum