let f, g be differentiable Function of REAL,REAL; :: thesis: (f - g) `| = (f `|) - (g `|)
let s be Element of REAL ; :: according to FUNCT_2:def 8 :: thesis: ((f - g) `|) . s = ((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;
thus ((f - g) `|) . s = diff ((f - g),s) by Th10
.= (diff (f,s)) - (diff (g,s)) by A1, FDIFF_1:14
.= ((f `|) - (g `|)) . s by A2, VALUED_1:15 ; :: thesis: verum