let r be Real; :: thesis: for f being PartFunc of REAL ,REAL st right_open_halfline r c= dom f & f is_differentiable_on right_open_halfline r & ( for x0 being Real st x0 in right_open_halfline r holds
0 < diff f,x0 ) holds
( f | (right_open_halfline r) is increasing & f | (right_open_halfline r) is one-to-one )
let f be PartFunc of REAL ,REAL ; :: thesis: ( right_open_halfline r c= dom f & f is_differentiable_on right_open_halfline r & ( for x0 being Real st x0 in right_open_halfline r holds
0 < diff f,x0 ) implies ( f | (right_open_halfline r) is increasing & f | (right_open_halfline r) is one-to-one ) )
assume Z: right_open_halfline r c= dom f ; :: thesis: ( not f is_differentiable_on right_open_halfline r or ex x0 being Real st
( x0 in right_open_halfline r & not 0 < diff f,x0 ) or ( f | (right_open_halfline r) is increasing & f | (right_open_halfline r) is one-to-one ) )
assume A1: ( f is_differentiable_on right_open_halfline r & ( for x0 being Real st x0 in right_open_halfline r holds
0 < diff f,x0 ) ) ; :: thesis: ( f | (right_open_halfline r) is increasing & f | (right_open_halfline r) is one-to-one )

now

let r1, r2 be Real; :: thesis: ( r1 in (right_open_halfline r) /\ (dom f) & r2 in (right_open_halfline r) /\ (dom f) & r1 < r2 implies f . r1 < f . r2 )
assume A2: ( r1 in (right_open_halfline r) /\ (dom f) & r2 in (right_open_halfline r) /\ (dom f) & r1 < r2 ) ; :: thesis: f . r1 < f . r2
then A3: ( r1 in right_open_halfline r & r1 in dom f & r2 in right_open_halfline r & r2 in dom f & r1 < r2 ) by XBOOLE_0:def 4;
set rr = max r1,r2;
A4: ].r,((max r1,r2) + 1).[ c= right_open_halfline r by XXREAL_1:247;
r1 in { g where g is Real : r < g } by A3, XXREAL_1:230;
then A5: ex g1 being Real st
( g1 = r1 & r < g1 ) ;
r2 in { p where p is Real : r < p } by A3, XXREAL_1:230;
then A6: ex g2 being Real st
( g2 = r2 & r < g2 ) ;
A7: r1 + 0 < (max r1,r2) + 1 by XREAL_1:10, XXREAL_0:25;
then r1 in { g1 where g1 is Real : ( r < g1 & g1 < (max r1,r2) + 1 ) } by A5;
then A8: r1 in ].r,((max r1,r2) + 1).[ by RCOMP_1:def 2;
A9: r < (max r1,r2) + 1 by A5, A7, XXREAL_0:2;
A10: f is_differentiable_on ].r,((max r1,r2) + 1).[ by A1, A4, FDIFF_1:34;
X11: ].r,((max r1,r2) + 1).[ c= dom f by Z, A4, XBOOLE_1:1;
for g1 being Real st g1 in ].r,((max r1,r2) + 1).[ holds
0 < diff f,g1 by A1, A4;
then A11: f | ].r,((max r1,r2) + 1).[ is increasing by A9, A10, X11, ROLLE:9;
r2 + 0 < (max r1,r2) + 1 by XREAL_1:10, XXREAL_0:25;
then r2 in { g2 where g2 is Real : ( r < g2 & g2 < (max r1,r2) + 1 ) } by A6;
then r2 in ].r,((max r1,r2) + 1).[ by RCOMP_1:def 2;
then A12: r2 in ].r,((max r1,r2) + 1).[ /\ (dom f) by A3, XBOOLE_0:def 4;
r1 in ].r,((max r1,r2) + 1).[ /\ (dom f) by A3, A8, XBOOLE_0:def 4;
hence f . r1 < f . r2 by A2, A11, A12, RFUNCT_2:43; :: thesis: verum

end;

hence f | (right_open_halfline r) is increasing by RFUNCT_2:43; :: thesis: f | (right_open_halfline r) is one-to-one
hence f | (right_open_halfline r) is one-to-one by FCONT_3:16; :: thesis: verum