let h be Function of REAL,REAL; :: thesis: ( h = f - g implies h is differentiable )
assume A2: 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 A2, FDIFF_1:14; :: thesis: verum