theorem :: ASYMPT_3:34

for f, g being Function of NAT,REAL holds
( f negligibleEQ g iff f - g is negligible )