set h = Gr2Iso (f,g);
let a, b be Element of (product <*G1,G2*>); :: according to GROUP_6:def 6 :: thesis: (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; :: thesis: verum