for X, Y, W being RealNormSpace
for Z being Subset of [:X,Y:]
for f, g being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`1 Z & g is_partial_differentiable_on`1 Z holds
( f + g is_partial_differentiable_on`1 Z & (f + g) `partial`1| Z = (f `partial`1| Z) + (g `partial`1| Z) )