for n being Nat
for k being non zero Real
for m being odd Integer holds (k to_power m) to_power n = k to_power (m * n)