for f being constant Function of REAL,REAL holds f `| = REAL --> 0