for p being prime Nat
for G being finite Group
for a, b being Element of G st G is p -commutative-group-like holds
for n being Nat holds (a * b) |^ (p |^ n) = (a |^ (p |^ n)) * (b |^ (p |^ n))