theorem :: FDIFF_2:45

for f being one-to-one PartFunc of REAL,REAL st [#] REAL c= dom f & f is_differentiable_on [#] REAL & ( for x0 being Real holds 0 < diff (f,x0) or for x0 being Real holds diff (f,x0) < 0 ) holds
( f is one-to-one & f " is_differentiable_on dom (f ") & ( for x0 being Real st x0 in dom (f ") holds
diff ((f "),x0) = 1 / (diff (f,((f ") . x0))) ) )