for n being Nat
for G being finite Group
for a being Element of G holds (a |^ n) " = a |^ ((card G) - (n mod (card G)))