theorem Th10: :: POLYDIFF:10
for r being Real
for f being differentiable Function of REAL,REAL holds (f `|) . r = diff (f,r)