let G1, G2, G3 be non empty multMagma ; 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; 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; 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; <*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
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; verum