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