theorem :: NDIFF_4:20

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
f | X is continuous