the negligible Function of NAT,REAL in negligibleFuncs by Def1;
hence not negligibleFuncs is empty ; :: thesis: verum