for g being polynomially-abs-bounded Function of NAT,REAL ex d being non empty positive-yielding XFinSequence of REAL ex N being Nat st
for x being Nat st N <= x holds
|.(g . x).| <= (polynom d) . x