for L being non empty unital associative multMagma
for x being Element of L
for n, m being Nat holds (power L) . (x,(n * m)) = (power L) . (((power L) . (x,n)),m)