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*>;
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;
A1: ( 1 in {1,2,3} & 2 in {1,2,3} & 3 in {1,2,3} ) by ENUMSET1:def 1;
A2: ( l . 1 = x1 & l . 2 = y1 & l . 3 = z1 & p . 1 = x2 & p . 2 = y2 & p . 3 = z2 & <*G1,G2,G3*> . 1 = G1 & <*G1,G2,G3*> . 2 = G2 & <*G1,G2,G3*> . 3 = G3 ) by FINSEQ_1:62;
dom lpl = dom (Carrier <*G1,G2,G3*>) by CARD_3:18
.= Seg 3 by FINSEQ_3:1, PARTFUN1:def 4 ;
then A3: len lpl = 3 by FINSEQ_1:def 3;
A4: len lpp = 3 by FINSEQ_1:62;
A5: ( lpp . 1 = x1 * x2 & lpp . 2 = y1 * y2 & lpp . 3 = z1 * z2 ) by FINSEQ_1:62;
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 )
A6: k in NAT by ORDINAL1:def 13;
assume ( 1 <= k & k <= 3 ) ; :: thesis: lpl . k = lpp . k
then A7: k in Seg 3 by A6;

per cases ( k = 1 or k = 2 or k = 3 ) by A7, ENUMSET1:def 1, FINSEQ_3:1;

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;

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

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

end;

end;

end;

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