set h = Gr2Iso f,g;
now let a,
b be
Element of
(product <*G1,G2*>);
(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:61;
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:61;
then
a2 * b2 = <*r1,r2*> . 2
by A6, A5, Lm2, GROUP_7:4;
then A8:
g . r2 =
g . (a2 * b2)
by FINSEQ_1:61
.=
(g . a2) * (g . b2)
by GROUP_6:def 7
;
A9:
b . 1
= b1
by A3, FINSEQ_1:61;
(
G1 = <*G1,G2*> . 1 &
a . 1
= a1 )
by A1, FINSEQ_1:61;
then
a1 * b1 = <*r1,r2*> . 1
by A6, A9, Lm1, GROUP_7:4;
then f . r1 =
f . (a1 * b1)
by FINSEQ_1:61
.=
(f . a1) * (f . b1)
by GROUP_6:def 7
;
hence
(Gr2Iso f,g) . (a * b) = ((Gr2Iso f,g) . a) * ((Gr2Iso f,g) . b)
by A2, A4, A7, A8, GROUP_7:32;
verum end;
hence
Gr2Iso f,g is Homomorphism of (product <*G1,G2*>),(product <*H1,H2*>)
by GROUP_6:def 7; verum