for m being Nat st 2 <= m holds
for A being Real ex n being positive Nat st A <= m |^ n