theorem Th14: :: PDIFF_9:14

for m, n being non zero Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),(REAL n) st X is open holds
( f is_differentiable_on X iff ( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_differentiable_in x ) ) ) by PDIFF_6:32;