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

now

let r1, r2 be Real; :: thesis: ( r1 in (left_open_halfline r) /\ (dom f) & r2 in (left_open_halfline r) /\ (dom f) & r1 < r2 implies f . r2 <= f . r1 )
assume A2: ( r1 in (left_open_halfline r) /\ (dom f) & r2 in (left_open_halfline r) /\ (dom f) & r1 < r2 ) ; :: thesis: f . r2 <= f . r1
then A3: ( r1 in left_open_halfline r & r1 in dom f & r2 in left_open_halfline r & r2 in dom f & r1 < r2 ) by XBOOLE_0:def 4;
set rr = min r1,r2;
A4: ].((min r1,r2) - 1),r.[ c= left_open_halfline r by XXREAL_1:263;
r1 in { g where g is Real : g < r } by A3, XXREAL_1:229;
then A5: ex g1 being Real st
( g1 = r1 & g1 < r ) ;
r2 in { p where p is Real : p < r } by A3, XXREAL_1:229;
then A6: ex g2 being Real st
( g2 = r2 & g2 < r ) ;
A7: ( min r1,r2 <= r1 & min r1,r2 <= r2 ) by XXREAL_0:17;
then A8: (min r1,r2) - 1 < r1 - 0 by XREAL_1:17;
then r1 in { g1 where g1 is Real : ( (min r1,r2) - 1 < g1 & g1 < r ) } by A5;
then A9: r1 in ].((min r1,r2) - 1),r.[ by RCOMP_1:def 2;
A10: (min r1,r2) - 1 < r by A5, A8, XXREAL_0:2;
A11: f is_differentiable_on ].((min r1,r2) - 1),r.[ by A1, A4, FDIFF_1:34;
X12: ].((min r1,r2) - 1),r.[ c= dom f by Z, A4, XBOOLE_1:1;
for g1 being Real st g1 in ].((min r1,r2) - 1),r.[ holds
diff f,g1 <= 0 by A1, A4;
then A12: f | ].((min r1,r2) - 1),r.[ is non-increasing by A10, A11, X12, ROLLE:12;
(min r1,r2) - 1 < r2 - 0 by A7, XREAL_1:17;
then r2 in { g2 where g2 is Real : ( (min r1,r2) - 1 < g2 & g2 < r ) } by A6;
then r2 in ].((min r1,r2) - 1),r.[ by RCOMP_1:def 2;
then A13: r2 in ].((min r1,r2) - 1),r.[ /\ (dom f) by A3, XBOOLE_0:def 4;
r1 in ].((min r1,r2) - 1),r.[ /\ (dom f) by A3, A9, XBOOLE_0:def 4;
hence f . r2 <= f . r1 by A2, A12, A13, RFUNCT_2:46; :: thesis: verum

end;

hence f | (left_open_halfline r) is non-increasing by RFUNCT_2:46; :: thesis: verum