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 ;
A3: <*G1,G2,G3*> . 3 = G3 ;
A4: <*G1,G2,G3*> . 2 = G2 ;
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 ;
A7: l . 3 = z1 ;
A8: l . 2 = y1 ;
A12: p . 3 = z2 ;
A13: p . 2 = y2 ;
A14: p . 1 = x2 ;
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 A17, A18;

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

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

hence lpl . k = lpp . k by A15, A6, A14, A2, Th1; :: thesis: verum

end;

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

hence lpl . k = lpp . k by A5, A8, A13, A4, Th1; :: thesis: verum

end;

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

hence lpl . k = lpp . k by A1, A7, A12, A3, Th1; :: thesis: verum

end;

end;

end;

dom lpl = dom (Carrier <*G1,G2,G3*>) by CARD_3:9
.= Seg 3 by FINSEQ_3:1, PARTFUN1:def 2 ;
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 A20, A16; :: thesis: verum