theorem Th60: :: PDIFF_9:60

for m being non zero Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for i being Nat st X is open & 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) ) )