theorem :: FDIFF_12:38

for f being PartFunc of REAL,REAL
for I, J being non empty Interval st f is_differentiable_on_interval I & J c= I & inf J < sup J holds
( f is_differentiable_on_interval J & ( for x being Real st x in J holds
(f `\ I) . x = (f `\ J) . x ) )