theorem Th6: :: FIB_NUM2:6
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)