theorem Th55: :: PDIFF_9:55

for m being non zero Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL st X c= dom f & f is_differentiable_on X holds
X is open