:: deftheorem defines `| POLYDIFF:def 1 :
for f being differentiable Function of REAL,REAL holds f `| = f `| REAL;