theorem Th19: :: POLYDIFF:19
for r being Real
for f being differentiable Function of REAL,REAL holds (r (#) f) `| = r (#) (f `|)