theorem Th4: :: NDIFF_4:4

for X being set
for n being non zero Element of NAT
for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X holds
X is Subset of REAL by XBOOLE_1:1;