theorem Th24: :: FDIFF_1:24

for f being PartFunc of REAL,REAL
for x0 being Real st f is_differentiable_in x0 holds
f is_continuous_in x0