let G1, G2 be non empty multMagma ; :: thesis: for x1, x2 being Element of G1
for y1, y2 being Element of G2 holds <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*>
let x1, x2 be Element of G1; :: thesis: for y1, y2 being Element of G2 holds <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*>
let y1, y2 be Element of G2; :: thesis: <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*>
set G = <*G1,G2*>;
reconsider l = <*x1,y1*>, p = <*x2,y2*>, lpl = <*x1,y1*> * <*x2,y2*>, lpp = <*(x1 * x2),(y1 * y2)*> as Element of product (Carrier <*G1,G2*>) by Def2;
A1: ( 1 in {1,2} & 2 in {1,2} ) by TARSKI:def 2;
A2: ( l . 1 = x1 & l . 2 = y1 & p . 1 = x2 & p . 2 = y2 & <*G1,G2*> . 1 = G1 & <*G1,G2*> . 2 = G2 ) by FINSEQ_1:61;
dom lpl = dom (Carrier <*G1,G2*>) by CARD_3:18
.= Seg 2 by FINSEQ_1:4, PARTFUN1:def 4 ;
then A3: len lpl = 2 by FINSEQ_1:def 3;
A4: len lpp = 2 by FINSEQ_1:61;
A5: ( lpp . 1 = x1 * x2 & lpp . 2 = y1 * y2 ) by FINSEQ_1:61;
for k being Nat st 1 <= k & k <= 2 holds
lpl . k = lpp . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= 2 implies lpl . k = lpp . k )
A6: k in NAT by ORDINAL1:def 13;
assume ( 1 <= k & k <= 2 ) ; :: thesis: lpl . k = lpp . k
then A7: k in Seg 2 by A6;

per cases ( k = 1 or k = 2 ) by A7, FINSEQ_1:4, TARSKI:def 2;

suppose k = 1 ; :: thesis: lpl . k = lpp . k

hence lpl . k = lpp . k by A1, A2, A5, Th4; :: thesis: verum

end;

suppose k = 2 ; :: thesis: lpl . k = lpp . k

hence lpl . k = lpp . k by A1, A2, A5, Th4; :: thesis: verum

end;

end;

end;

hence <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*> by A3, A4, FINSEQ_1:18; :: thesis: verum