:: deftheorem defneg defines negligible ASYMPT_3:def 4 :
for f being Function of NAT,REAL holds
( f is negligible iff for c being non empty positive-yielding XFinSequence of REAL ex N being Nat st
for x being Nat st N <= x holds
|.(f . x).| < 1 / ((polynom c) . x) );