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:13
.= ((f `|) + (g `|)) . s by A2, VALUED_1:1 ; :: thesis: verum