:: deftheorem defines negligibleEQ ASYMPT_3:def 6 :
for f, g being Function of NAT,REAL holds
( f negligibleEQ g iff ex h being Function of NAT,REAL st
( h is negligible & ( for x being Nat holds |.((f . x) - (g . x)).| <= |.(h . x).| ) ) );