let f, g be differentiable Function of REAL,REAL; :: thesis: (f (#) g) `| = (g (#) (f `|)) + (f (#) (g `|))
let s be Element of REAL ; :: according to FUNCT_2:def 8 :: thesis: ((f (#) g) `|) . s = ((g (#) (f `|)) + (f (#) (g `|))) . s
A1: ( f is_differentiable_in s & g is_differentiable_in s ) by Th9;
A2: ( (f `|) . s = diff (f,s) & (g `|) . s = diff (g,s) ) by Th10;
A3: ( (g . s) * ((f `|) . s) = (g (#) (f `|)) . s & (f . s) * ((g `|) . s) = (f (#) (g `|)) . s ) by VALUED_1:5;
thus ((f (#) g) `|) . s = diff ((f (#) g),s) by Th10
.= ((g . s) * (diff (f,s))) + ((f . s) * (diff (g,s))) by A1, FDIFF_1:16
.= ((g (#) (f `|)) + (f (#) (g `|))) . s by A2, A3, VALUED_1:1 ; :: thesis: verum