for m, k being Nat st 1 <= m holds
1 <= m to_power k