let p, g be Real; :: thesis: for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f,x) <= 0 ) holds
f | ].p,g.[ is non-increasing
let f be PartFunc of REAL,REAL; :: thesis: ( ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f,x) <= 0 ) implies f | ].p,g.[ is non-increasing )
assume that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x being Real st x in ].p,g.[ holds
diff (f,x) <= 0 ; :: thesis: f | ].p,g.[ is non-increasing

now :: thesis: for x1, x2 being Real st x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) & x1 < x2 holds
f . x2 <= f . x1

let x1, x2 be Real; :: thesis: ( x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) & x1 < x2 implies f . x2 <= f . x1 )
assume that
A4: ( x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) ) and
A5: x1 < x2 ; :: thesis: f . x2 <= f . x1
A6: 0 <= x2 - x1 by A5, XREAL_1:50;
reconsider Z = ].x1,x2.[ as open Subset of REAL ;
( x1 in ].p,g.[ & x2 in ].p,g.[ ) by A4, XBOOLE_0:def 4;
then A7: [.x1,x2.] c= ].p,g.[ by XXREAL_2:def 12;
f | ].p,g.[ is continuous by A2, FDIFF_1:25;
then A8: f | [.x1,x2.] is continuous by A7, FCONT_1:16;
A9: Z c= [.x1,x2.] by XXREAL_1:25;
then f is_differentiable_on Z by A2, A7, FDIFF_1:26, XBOOLE_1:1;
then A10: ex x0 being Real st
( x0 in ].x1,x2.[ & diff (f,x0) = ((f . x2) - (f . x1)) / (x2 - x1) ) by A1, A5, A7, A8, Th3, XBOOLE_1:1;
A11: 0 <> x2 - x1 by A5;
Z c= ].p,g.[ by A7, A9;
then (((f . x2) - (f . x1)) / (x2 - x1)) * (x2 - x1) <= 0 * (x2 - x1) by A3, A6, A10, XREAL_1:64;
then (f . x2) - (f . x1) <= 0 by A11, XCMPLX_1:87;
then f . x2 <= (f . x1) + 0 by XREAL_1:20;
hence f . x2 <= f . x1 ; :: thesis: verum

end;

hence f | ].p,g.[ is non-increasing by RFUNCT_2:23; :: thesis: verum