theorem Th7: :: CKSPACE1:7

for m being non zero Element of NAT
for Z being non empty Subset of (REAL m)
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 ^ I)) = (f `partial| (Z,G)) `partial| (Z,I)