theorem :: FDIFF_12:7

for f being PartFunc of REAL,REAL
for a, b being Real st a < b & f is_differentiable_on_interval ['a,b'] holds
f is_differentiable_on ].a,b.[