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 [#] 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 that
A1: f is_differentiable_on [#] REAL and
A2: for x0 being Real holds 0 < diff (f,x0) ; :: thesis: ( f | ([#] REAL) is increasing & f is one-to-one )

A3: now :: thesis: for r1, r2 being Real st r1 in ([#] REAL) /\ (dom f) & r2 in ([#] REAL) /\ (dom f) & r1 < r2 holds
f . r1 < f . r2

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

end;

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

now :: thesis: for r1, r2 being Element of REAL holds
( not r1 in dom f or not r2 in dom f or not f . r1 = f . r2 or not r1 <> r2 )

given r1, r2 being Element of REAL such that A14: r1 in dom f and
A15: r2 in dom f and
A16: f . r1 = f . r2 and
A17: r1 <> r2 ; :: thesis: contradiction
A18: r2 in ([#] REAL) /\ (dom f) by A15, XBOOLE_0:def 4;
A19: r1 in ([#] REAL) /\ (dom f) by A14, XBOOLE_0:def 4;

now :: thesis: contradiction

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

suppose r1 < r2 ; :: thesis: contradiction

hence contradiction by A3, A16, A19, A18; :: thesis: verum

end;

suppose r2 < r1 ; :: thesis: contradiction

hence contradiction by A3, A16, A19, A18; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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