theorem LM215: :: NDIFF_7:36

for X, Y, W being RealNormSpace
for z being Point of [:X,Y:]
for f1, f2 being PartFunc of [:X,Y:],W st f1 is_partial_differentiable_in`1 z & f2 is_partial_differentiable_in`1 z holds
( f1 + f2 is_partial_differentiable_in`1 z & partdiff`1 ((f1 + f2),z) = (partdiff`1 (f1,z)) + (partdiff`1 (f2,z)) & f1 - f2 is_partial_differentiable_in`1 z & partdiff`1 ((f1 - f2),z) = (partdiff`1 (f1,z)) - (partdiff`1 (f2,z)) )