theorem :: FDIFF_2:47

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