theorem :: NDIFF_4:19

for n being non zero Element of NAT
for f being PartFunc of REAL,(REAL n)
for x0 being Real st f is_differentiable_in x0 holds
f is_continuous_in x0 by NDIFF_3:22, NFCONT_4:def 1;