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

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

let x1, x2 be Element of REAL ; :: thesis: ( x1 in ].p,q.[ /\ (dom f) & x2 in ].p,q.[ /\ (dom f) implies f . x1 = f . x2 )
assume ( x1 in ].p,q.[ /\ (dom f) & x2 in ].p,q.[ /\ (dom f) ) ; :: thesis: f . x1 = f . x2
then A3: ( x1 in ].p,q.[ & x2 in ].p,q.[ ) by XBOOLE_0:def 4;

now :: thesis: f . x1 = f . x2

per cases ( x1 = x2 or x1 < x2 or x2 < x1 ) by XXREAL_0:1;

suppose x1 = x2 ; :: thesis: f . x1 = f . x2

hence f . x1 = f . x2 ; :: thesis: verum

end;

suppose A4: x1 < x2 ; :: thesis: f . x1 = f . x2

then 0 <> x2 - x1 ;
then A5: 0 <> (x2 - x1) " by XCMPLX_1:202;
reconsider Z = ].x1,x2.[ as open Subset of REAL ;
A6: [.x1,x2.] c= ].p,q.[ by A3, 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 A9: 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;
Z c= ].p,q.[ by A6, A8;
then 0 = (f . x2) - (f . x1) by A2, A5, A9, XCMPLX_1:6;
hence f . x1 = f . x2 ; :: thesis: verum

end;

suppose A10: x2 < x1 ; :: thesis: f . x1 = f . x2

then 0 <> x1 - x2 ;
then A11: 0 <> (x1 - x2) " by XCMPLX_1:202;
reconsider Z = ].x2,x1.[ as open Subset of REAL ;
A12: [.x2,x1.] c= ].p,q.[ by A3, XXREAL_2:def 12;
then A13: f | [.x2,x1.] is continuous by A1, FDIFF_1:25, FCONT_1:16;
A14: Z c= [.x2,x1.] by XXREAL_1:25;
then f is_differentiable_on Z by A1, A12, FDIFF_1:26, XBOOLE_1:1;
then A15: ex x0 being Real st
( x0 in ].x2,x1.[ & diff (f,x0) = ((f . x1) - (f . x2)) / (x1 - x2) ) by A1, A10, A12, A13, ROLLE:3, XBOOLE_1:1;
Z c= ].p,q.[ by A12, A14;
then 0 = (f . x1) - (f . x2) by A2, A11, A15, XCMPLX_1:6;
hence f . x1 = f . x2 ; :: thesis: verum

end;

end;

end;

hence f . x1 = f . x2 ; :: thesis: verum

end;

hence f | ].p,q.[ is constant by PARTFUN2:58; :: thesis: verum