let n be non zero Element of NAT ; :: thesis:
let Z be open Subset of REAL; :: thesis:
let f1, f2 be PartFunc of REAL,(REAL n); :: thesis:
assume that
A1: Z c= dom (f1 + f2) and
A2: ( f1 is_differentiable_on Z & f2 is_differentiable_on Z ) ; :: thesis:
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
A3: f1 + f2 = g1 + g2 by NFCONT_4:5;
A4: Z c= dom (g1 + g2) by A1, NFCONT_4:5;
A5: ( Z c= dom g1 & Z c= dom g2 ) by A2;

now :: thesis:

let x be Real; :: thesis:
assume x in Z ; :: thesis:
then f1 | Z is_differentiable_in x by A2;
hence g1 | Z is_differentiable_in x ; :: thesis:

end;

then A6: g1 is_differentiable_on Z by A5, NDIFF_3:def 5;

now :: thesis:

let x be Real; :: thesis:
assume x in Z ; :: thesis:
then f2 | Z is_differentiable_in x by A2;
hence g2 | Z is_differentiable_in x ; :: thesis:

end;

then g2 is_differentiable_on Z by A5, NDIFF_3:def 5;
then A7: ( g1 + g2 is_differentiable_on Z & ( for x being Real st x in Z holds
((g1 + g2) `| Z) . x = (diff (g1,x)) + (diff (g2,x)) ) ) by A4, A6, NDIFF_3:17;

now :: thesis:

let x be Real; :: thesis:
assume x in Z ; :: thesis:
then (g1 + g2) | Z is_differentiable_in x by A7, NDIFF_3:def 5;
hence (f1 + f2) | Z is_differentiable_in x by A3; :: thesis:

end;

hence A8: f1 + f2 is_differentiable_on Z by A1; :: thesis:
let x be Real; :: thesis:
assume A9: x in Z ; :: thesis:
then ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A2, Th5;
then ( f1 + f2 is_differentiable_in x & diff ((f1 + f2),x) = (diff (f1,x)) + (diff (f2,x)) ) by Th11;
hence ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) by A9, A8, Def4; :: thesis: