theorem Th70: :: PDIFF_9:70

for m being non zero Element of NAT
for Z being set
for i being Nat
for f being PartFunc of (REAL m),REAL holds
( f is_partial_differentiable_on Z,i iff f | Z is_partial_differentiable_on Z,i )