theorem :: GROUP_5:33

for n being Nat
for G being Group
for a, b being Element of G holds [.a,(b |^ n).] = ((b |^ a) |^ (- n)) * (b |^ n)