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

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

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

end;

hence f | ].p,q.[ is non-decreasing by RFUNCT_2:22; :: thesis: verum