theorem Th32: :: NDIFF14:32

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 being PartFunc of (product S),T st Z is open & f is_partial_differentiable_on Z,I holds
( - f is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((- f),Z,I,i) = - (PartDiffSeq (f,Z,I,i)) ) )