let m be non empty Element of NAT ; :: thesis: for X being Subset of (REAL m)
for f, g being PartFunc of (REAL m),REAL st X c= dom f & X c= dom g & f is_differentiable_on X & g is_differentiable_on X holds
( f + g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((f + g) `| X) /. x = ((f `| X) /. x) + ((g `| X) /. x) ) )
let X be Subset of (REAL m); :: thesis: for f, g being PartFunc of (REAL m),REAL st X c= dom f & X c= dom g & f is_differentiable_on X & g is_differentiable_on X holds
( f + g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((f + g) `| X) /. x = ((f `| X) /. x) + ((g `| X) /. x) ) )
let f, g be PartFunc of (REAL m),REAL; :: thesis: ( X c= dom f & X c= dom g & f is_differentiable_on X & g is_differentiable_on X implies ( f + g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((f + g) `| X) /. x = ((f `| X) /. x) + ((g `| X) /. x) ) ) )
assume AK: ( X c= dom f & X c= dom g ) ; :: thesis: ( not f is_differentiable_on X or not g is_differentiable_on X or ( f + g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((f + g) `| X) /. x = ((f `| X) /. x) + ((g `| X) /. x) ) ) )
assume AS1: ( f is_differentiable_on X & g is_differentiable_on X ) ; :: thesis: ( f + g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((f + g) `| X) /. x = ((f `| X) /. x) + ((g `| X) /. x) ) )
then P0: X is open by AK, YTh33;
dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
then P3: X c= dom (f + g) by AK, XBOOLE_1:19;

P5: now :: thesis: for x being Element of REAL m st x in X holds
( f + g is_differentiable_in x & diff ((f + g),x) = (diff (f,x)) + (diff (g,x)) )

let x be Element of REAL m; :: thesis: ( x in X implies ( f + g is_differentiable_in x & diff ((f + g),x) = (diff (f,x)) + (diff (g,x)) ) )
assume x in X ; :: thesis: ( f + g is_differentiable_in x & diff ((f + g),x) = (diff (f,x)) + (diff (g,x)) )
then ( f is_differentiable_in x & g is_differentiable_in x ) by AK, AS1, P0, YTh32;
hence ( f + g is_differentiable_in x & diff ((f + g),x) = (diff (f,x)) + (diff (g,x)) ) by PDIFF620X; :: thesis: verum

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 P3, P0, YTh32; :: thesis: for x being Element of REAL m st x in X holds
((f + g) `| X) /. x = ((f `| X) /. x) + ((g `| X) /. x)
let x be Element of REAL m; :: thesis: ( x in X implies ((f + g) `| X) /. x = ((f `| X) /. x) + ((g `| X) /. x) )
assume P7: x in X ; :: thesis: ((f + g) `| X) /. x = ((f `| X) /. x) + ((g `| X) /. x)
then ((f + g) `| X) /. x = diff ((f + g),x) by P3, XDef1;
then ((f + g) `| X) /. x = (diff (f,x)) + (diff (g,x)) by P7, P5;
then ((f + g) `| X) /. x = ((f `| X) /. x) + (diff (g,x)) by AK, P7, XDef1;
hence ((f + g) `| X) /. x = ((f `| X) /. x) + ((g `| X) /. x) by AK, P7, XDef1; :: thesis: verum