theorem Th73: :: PDIFF_9:73

for m being non zero Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL
for I, G being non empty FinSequence of NAT st f is_partial_differentiable_on Z,G holds
for n being Nat st n <= len I holds
(PartDiffSeq ((f `partial| (Z,G)),Z,I)) . n = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + n)