theorem :: NDIFF_7:24

for G being RealNormSpace-Sequence
for F being RealNormSpace
for i being set
for f, g being PartFunc of (product G),F
for X being Subset of (product G) st X is open & i in dom G & 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)) )