theorem :: POLYDIFF:17

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