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

A4: now

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

end;

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

now

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

now

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

suppose r1 < r2 ; :: thesis: contradiction

hence contradiction by A4, A17, A20, A19; :: thesis: verum

end;

suppose r2 < r1 ; :: thesis: contradiction

hence contradiction by A4, A17, A20, A19; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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