theorem Th82: :: PDIFF_9:82

for m being non zero Element of NAT
for f being PartFunc of (REAL m),REAL
for Z being Subset of (REAL m)
for i being Element of NAT st Z is open & 1 <= i & i <= m & f is_partial_differentiable_on Z,i holds
f `partial| (Z,<*i*>) = f `partial| (Z,i)