theorem :: NDIFF14:33

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for I being non empty FinSequence of dom S
for f, g being PartFunc of (product S),T st Z is open & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I holds
( f - g is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f - g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) - (PartDiffSeq (g,Z,I,i)) ) )