let m, n be non zero Element of NAT ; :: thesis: for X being Subset of (REAL m)
for f, g being PartFunc of (REAL m),(REAL n) st 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 = (diff (f,x)) - (diff (g,x)) ) )
let X be Subset of (REAL m); :: thesis: for f, g being PartFunc of (REAL m),(REAL n) st 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 = (diff (f,x)) - (diff (g,x)) ) )
let f, g be PartFunc of (REAL m),(REAL n); :: thesis: ( 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 = (diff (f,x)) - (diff (g,x)) ) ) )
assume A1: ( 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 = (diff (f,x)) - (diff (g,x)) ) )
then A2: X is open by Th13;
then A3: ( X c= dom f & X c= dom g ) by A1, Th14;
dom (f - g) = (dom f) /\ (dom g) by VALUED_2:def 46;
then A4: X c= dom (f - g) by A3, XBOOLE_1:19;

now :: thesis: for x being Element of REAL m st x in X holds
f - g is_differentiable_in x

let x be Element of REAL m; :: thesis: ( x in X implies f - g is_differentiable_in x )
assume x in X ; :: thesis: f - g is_differentiable_in x
then ( f is_differentiable_in x & g is_differentiable_in x ) by A1, A2, Th14;
hence f - g is_differentiable_in x by PDIFF_6:21; :: thesis: verum

end;

hence f - g is_differentiable_on X by A4, A2, Th14; :: thesis: for x being Element of REAL m st x in X holds
((f - g) `| X) /. x = (diff (f,x)) - (diff (g,x))
let x be Element of REAL m; :: thesis: ( x in X implies ((f - g) `| X) /. x = (diff (f,x)) - (diff (g,x)) )
assume A5: x in X ; :: thesis: ((f - g) `| X) /. x = (diff (f,x)) - (diff (g,x))
then ( f is_differentiable_in x & g is_differentiable_in x ) by A1, A2, Th14;
then diff ((f - g),x) = (diff (f,x)) - (diff (g,x)) by PDIFF_6:21;
hence ((f - g) `| X) /. x = (diff (f,x)) - (diff (g,x)) by A4, A5, Def1; :: thesis: verum