for n being Nat
for a being non trivial Nat
for x being positive Nat st a > (2 * n) * (x |^ n) holds
( (x |^ n) - (1 / 2) < (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) & (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) < (x |^ n) + (1 / 2) )