for a being Real
for k being Nat ex c being non empty positive-yielding XFinSequence of REAL st
for x being Nat holds a * (x to_power k) <= (polynom c) . x