theorem :: FDIFF_12:12

for f being PartFunc of REAL,REAL
for I being non empty Interval st I is open_interval holds
( f is_differentiable_on I iff f is_differentiable_on_interval I )