theorem PXR2: :: ASYMPT_3:23

for f being Function of NAT,REAL st f is negligible holds
for r being Real st 0 < r holds
ex N being Nat st
for x being Nat st N <= x holds
|.(f . x).| < r