theorem LM216: :: NDIFF_7:37

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`2 z & f2 is_partial_differentiable_in`2 z holds
( f1 + f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 + f2),z) = (partdiff`2 (f1,z)) + (partdiff`2 (f2,z)) & f1 - f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 - f2),z) = (partdiff`2 (f1,z)) - (partdiff`2 (f2,z)) )