theorem :: ASYMPT_2:1

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