theorem :: GROUP_5:32

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