for m being non zero Element of NAT
for X being Subset of (REAL m)
for I being non empty FinSequence of NAT
for f, g being PartFunc of (REAL m),REAL st X is open & rng I c= Seg m & f is_partial_differentiable_on X,I & g is_partial_differentiable_on X,I holds
( f + g is_partial_differentiable_on X,I & (f + g) `partial| (X,I) = (f `partial| (X,I)) + (g `partial| (X,I)) )