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