let H be Subgroup of G; H is p -commutative-group-like
let a, b be Element of H; GROUPP_1:def 3 (a * b) |^ p = (a |^ p) * (b |^ p)
reconsider a2 = a, b2 = b as Element of G by GROUP_2:51;
A2:
a * b = a2 * b2
by GROUP_8:2;
A3:
( a |^ p = a2 |^ p & b |^ p = b2 |^ p )
by GROUP_8:4;
thus (a * b) |^ p =
(a2 * b2) |^ p
by A2, GROUP_8:4
.=
(a2 |^ p) * (b2 |^ p)
by def3
.=
(a |^ p) * (b |^ p)
by A3, GROUP_8:2
; verum