let m be non zero Element of NAT ; :: thesis:
let X be Subset of (REAL m); :: thesis:
let f, g be PartFunc of (REAL m),REAL; :: thesis:
assume A1: ( X c= dom f & X c= dom g ) ; :: thesis:
assume A2: ( f is_differentiable_on X & g is_differentiable_on X ) ; :: thesis:
then A3: X is open by A1, Th55;
dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
then A4: X c= dom (f + g) by A1, XBOOLE_1:19;

A5: now :: thesis:

let x be Element of REAL m; :: thesis:
assume x in X ; :: thesis:
then ( f is_differentiable_in x & g is_differentiable_in x ) by A1, A2, A3, Th54;
hence ( f + g is_differentiable_in x & diff ((f + g),x) = (diff (f,x)) + (diff (g,x)) ) by Th51; :: thesis:

end;

then for x being Element of REAL m st x in X holds
f + g is_differentiable_in x ;
hence f + g is_differentiable_on X by A4, A3, Th54; :: thesis:
let x be Element of REAL m; :: thesis:
assume A6: x in X ; :: thesis:
then ((f + g) `| X) /. x = diff ((f + g),x) by A4, Def4;
then ((f + g) `| X) /. x = (diff (f,x)) + (diff (g,x)) by A6, A5;
then ((f + g) `| X) /. x = ((f `| X) /. x) + (diff (g,x)) by A1, A6, Def4;
hence ((f + g) `| X) /. x = ((f `| X) /. x) + ((g `| X) /. x) by A1, A6, Def4; :: thesis: