theorem :: PDIFF_9:15

for m, n being non zero Element of NAT
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)) ) )