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

.= 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

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

dom lpl =
dom (Carrier <*G1,G2,G3*>)
by CARD_3:9
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;

end;assume that

A17: 1 <= k and

A18: k <= 3 ; :: thesis: lpl . k = lpp . k

A19: k in Seg 3 by A17, A18;

.= 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