theorem :: FDIFF_12:18

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