theorem :: PDIFF_6:20

for n, m being non zero Nat
for g1, g2 being PartFunc of (REAL m),(REAL n)
for y0 being Element of REAL m st g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds
( g1 + g2 is_differentiable_in y0 & diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) )