theorem :: POLYDIFF:18

for r being Real
for f being differentiable Function of REAL,REAL holds (f - r) `| = f `|