theorem Th51: :: PDIFF_9:51

for m being non zero Element of NAT
for f, g being PartFunc of (REAL m),REAL
for x being Element of REAL m st f is_differentiable_in x & g is_differentiable_in x holds
( f + g is_differentiable_in x & diff ((f + g),x) = (diff (f,x)) + (diff (g,x)) & f - g is_differentiable_in x & diff ((f - g),x) = (diff (f,x)) - (diff (g,x)) )