set h = Gr2Iso (f,g);
let a, b be Element of (product <*G1,G2*>); GROUP_6:def 6 (Gr2Iso (f,g)) . (a * b) = ((Gr2Iso (f,g)) . a) * ((Gr2Iso (f,g)) . b)
consider a1 being Element of G1, a2 being Element of G2 such that
A1:
a = <*a1,a2*>
and
A2:
(Gr2Iso (f,g)) . a = <*(f . a1),(g . a2)*>
by Def1;
consider b1 being Element of G1, b2 being Element of G2 such that
A3:
b = <*b1,b2*>
and
A4:
(Gr2Iso (f,g)) . b = <*(f . b1),(g . b2)*>
by Def1;
A5:
b . 2 = b2
by A3, FINSEQ_1:44;
consider r1 being Element of G1, r2 being Element of G2 such that
A6:
a * b = <*r1,r2*>
and
A7:
(Gr2Iso (f,g)) . (a * b) = <*(f . r1),(g . r2)*>
by Def1;
( G2 = <*G1,G2*> . 2 & a . 2 = a2 )
by A1, FINSEQ_1:44;
then
a2 * b2 = <*r1,r2*> . 2
by A6, A5, Lm2, GROUP_7:1;
then A8: g . r2 =
g . (a2 * b2)
by FINSEQ_1:44
.=
(g . a2) * (g . b2)
by GROUP_6:def 6
;
A9:
b . 1 = b1
by A3, FINSEQ_1:44;
( G1 = <*G1,G2*> . 1 & a . 1 = a1 )
by A1, FINSEQ_1:44;
then
a1 * b1 = <*r1,r2*> . 1
by A6, A9, Lm1, GROUP_7:1;
then f . r1 =
f . (a1 * b1)
by FINSEQ_1:44
.=
(f . a1) * (f . b1)
by GROUP_6:def 6
;
hence
(Gr2Iso (f,g)) . (a * b) = ((Gr2Iso (f,g)) . a) * ((Gr2Iso (f,g)) . b)
by A2, A4, A7, A8, GROUP_7:29; verum