let g1, g2 be Element of (Image g); GROUPP_1:def 3 (g1 * g2) |^ p = (g1 |^ p) * (g2 |^ p)
reconsider h1 = g1, h2 = g2 as Element of H by GROUP_2:42;
g1 in Image g
;
then consider a being Element of G such that
A1:
g1 = g . a
by GROUP_6:45;
g2 in Image g
;
then consider b being Element of G such that
A2:
g2 = g . b
by GROUP_6:45;
g1 * g2 =
h1 * h2
by GROUP_2:43
.=
g . (a * b)
by A1, A2, GROUP_6:def 6
;
then A3: (g1 * g2) |^ p =
(g . (a * b)) |^ p
by GROUP_8:4
.=
g . ((a * b) |^ p)
by GROUP_6:37
.=
g . ((a |^ p) * (b |^ p))
by Def3
.=
(g . (a |^ p)) * (g . (b |^ p))
by GROUP_6:def 6
.=
((g . a) |^ p) * (g . (b |^ p))
by GROUP_6:37
.=
(h1 |^ p) * (h2 |^ p)
by A1, A2, GROUP_6:37
;
( h1 |^ p = g1 |^ p & h2 |^ p = g2 |^ p )
by GROUP_8:4;
hence
(g1 * g2) |^ p = (g1 |^ p) * (g2 |^ p)
by A3, GROUP_2:43; verum