theorem Th15: :: POLYDIFF:15

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