theorem :: AOFA_I00:13

for x being Real
for n, m being Nat holds (x to_power n) to_power m = x to_power (n * m) by NEWTON:9;