let h be Function of REAL,REAL; :: thesis: ( h = f + g implies h is differentiable )
assume A1: h = f + g ; :: thesis: h is differentiable
let r be Real; :: according to POLYDIFF:def 2 :: thesis: h is_differentiable_in r
( f is_differentiable_in r & g is_differentiable_in r ) by Th9;
hence h is_differentiable_in r by A1, FDIFF_1:13; :: thesis: verum