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*>;
A1: <*G1,G2*> . 1 = G1 by FINSEQ_1:61;
A2: <*G1,G2*> . 2 = G2 by FINSEQ_1:61;
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;
A3: 2 in {1,2} by TARSKI:def 2;
A4: l . 1 = x1 by FINSEQ_1:61;
A5: lpp . 1 = x1 * x2 by FINSEQ_1:61;
A6: p . 2 = y2 by FINSEQ_1:61;
A7: lpp . 2 = y1 * y2 by FINSEQ_1:61;
A8: p . 1 = x2 by FINSEQ_1:61;
A9: l . 2 = y1 by FINSEQ_1:61;
A10: 1 in {1,2} by TARSKI:def 2;
A11: 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 )
assume that
A12: 1 <= k and
A13: k <= 2 ; :: thesis: lpl . k = lpp . k
k in NAT by ORDINAL1:def 13;
then A14: k in Seg 2 by A12, A13;

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

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

hence lpl . k = lpp . k by A10, A4, A8, A1, A5, Th4; :: thesis: verum

end;

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

hence lpl . k = lpp . k by A3, A9, A6, A2, A7, Th4; :: thesis: verum

end;

end;

end;

dom lpl = dom (Carrier <*G1,G2*>) by CARD_3:18
.= Seg 2 by FINSEQ_1:4, PARTFUN1:def 4 ;
then A15: len lpl = 2 by FINSEQ_1:def 3;
len lpp = 2 by FINSEQ_1:61;
hence <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*> by A15, A11, FINSEQ_1:18; :: thesis: verum