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