theorem Th76: :: PDIFF_9:76

for m being non zero Element of NAT
for X being Subset of (REAL m)
for I being non empty FinSequence of NAT
for f, g being PartFunc of (REAL m),REAL st X is open & rng I c= Seg m & f is_partial_differentiable_on X,I & g is_partial_differentiable_on X,I holds
for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((f - g),X,I)) . i is_partial_differentiable_on X,I /. (i + 1) & (PartDiffSeq ((f - g),X,I)) . i = ((PartDiffSeq (f,X,I)) . i) - ((PartDiffSeq (g,X,I)) . i) )