theorem :: FDIFF_12:37

for f being PartFunc of REAL,REAL
for I being non empty Interval st f is_differentiable_on_interval I holds
f | I is continuous