theorem :: BINOM:11

for R being non empty unital associative multMagma
for a being Element of R
for n, m being Nat holds (a |^ n) |^ m = a |^ (n * m)