let G1, G2, G3 be non empty multMagma ; :: thesis: for x1, x2 being Element of G1
for y1, y2 being Element of G2
for z1, z2 being Element of G3 holds <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*>

let x1, x2 be Element of G1; :: thesis: for y1, y2 being Element of G2
for z1, z2 being Element of G3 holds <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*>

let y1, y2 be Element of G2; :: thesis: for z1, z2 being Element of G3 holds <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*>
let z1, z2 be Element of G3; :: thesis: <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*>
set G = <*G1,G2,G3*>;
A1: 3 in {1,2,3} by ENUMSET1:def 1;
A2: <*G1,G2,G3*> . 1 = G1 by FINSEQ_1:45;
A3: <*G1,G2,G3*> . 3 = G3 by FINSEQ_1:45;
A4: <*G1,G2,G3*> . 2 = G2 by FINSEQ_1:45;
reconsider l = <*x1,y1,z1*>, p = <*x2,y2,z2*>, lpl = <*x1,y1,z1*> * <*x2,y2,z2*>, lpp = <*(x1 * x2),(y1 * y2),(z1 * z2)*> as Element of product (Carrier <*G1,G2,G3*>) by Def2;
A5: 2 in {1,2,3} by ENUMSET1:def 1;
A6: l . 1 = x1 by FINSEQ_1:45;
A7: l . 3 = z1 by FINSEQ_1:45;
A8: l . 2 = y1 by FINSEQ_1:45;
A9: lpp . 3 = z1 * z2 by FINSEQ_1:45;
A10: lpp . 2 = y1 * y2 by FINSEQ_1:45;
A11: lpp . 1 = x1 * x2 by FINSEQ_1:45;
A12: p . 3 = z2 by FINSEQ_1:45;
A13: p . 2 = y2 by FINSEQ_1:45;
A14: p . 1 = x2 by FINSEQ_1:45;
A15: 1 in {1,2,3} by ENUMSET1:def 1;
A16: for k being Nat st 1 <= k & k <= 3 holds
lpl . k = lpp . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= 3 implies lpl . k = lpp . k )
assume that
A17: 1 <= k and
A18: k <= 3 ; :: thesis: lpl . k = lpp . k
A19: k in Seg 3 by ;
per cases ( k = 1 or k = 2 or k = 3 ) by ;
suppose k = 1 ; :: thesis: lpl . k = lpp . k
hence lpl . k = lpp . k by A15, A6, A14, A2, A11, Th1; :: thesis: verum
end;
suppose k = 2 ; :: thesis: lpl . k = lpp . k
hence lpl . k = lpp . k by A5, A8, A13, A4, A10, Th1; :: thesis: verum
end;
suppose k = 3 ; :: thesis: lpl . k = lpp . k
hence lpl . k = lpp . k by A1, A7, A12, A3, A9, Th1; :: thesis: verum
end;
end;
end;
dom lpl = dom (Carrier <*G1,G2,G3*>) by CARD_3:9
.= Seg 3 by ;
then A20: len lpl = 3 by FINSEQ_1:def 3;
len lpp = 3 by FINSEQ_1:45;
hence <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*> by ; :: thesis: verum