theorem :: PDIFF_9:88

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
(f `partial| (Z,G)) `partial| (Z,I) = f `partial| (Z,(G ^ I))