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

A2: now

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

end;

hence f | ([#] REAL ) is increasing by RFUNCT_2:43; :: thesis: f is one-to-one

now

given r1, r2 being Real such that A13: ( r1 in dom f & r2 in dom f & f . r1 = f . r2 ) and
A14: r1 <> r2 ; :: thesis: contradiction
A15: ( r1 in ([#] REAL ) /\ (dom f) & r2 in ([#] REAL ) /\ (dom f) ) by A13, XBOOLE_0:def 4;

now

per cases ( r1 < r2 or r2 < r1 ) by A14, XXREAL_0:1;

suppose r1 < r2 ; :: thesis: contradiction

hence contradiction by A2, A13, A15; :: thesis: verum

end;

suppose r2 < r1 ; :: thesis: contradiction

hence contradiction by A2, A13, A15; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence f is one-to-one by PARTFUN1:38; :: thesis: verum