for G being Group
for a, b being Element of G
for n being Nat holds (a |^ n) |^ b = (a |^ b) |^ n by Lm4;