theorem :: NDIFF14:29

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for f, g being PartFunc of (product S),T
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i holds
( f - g is_partial_differentiable_on Z,i & (f - g) `partial| (Z,i) = (f `partial| (Z,i)) - (g `partial| (Z,i)) )