let p, g be Real; :: thesis: ( p < g implies 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 V8() )
assume p < g ; :: 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 V8()
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 V8() )
assume that
A0: ].p,g.[ c= dom f and
A1: f is_differentiable_on ].p,g.[ and
A2: for x being Real st x in ].p,g.[ holds
diff f,x = 0 ; :: thesis: f | ].p,g.[ is V8()

now

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

now

per cases ( x1 = x2 or not x1 = x2 ) ;

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

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

end;

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

now

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

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

reconsider Z = ].x1,x2.[ as open Subset of REAL ;
A6: [.x1,x2.] c= ].p,g.[ by A3, XXREAL_2:def 12;
A7: Z c= [.x1,x2.] by XXREAL_1:25;
then A8: Z c= ].p,g.[ by A6, XBOOLE_1:1;
0 <> x2 - x1 by A5;
then A9: 0 <> (x2 - x1) " by XCMPLX_1:203;
f | ].p,g.[ is continuous by A1, FDIFF_1:33;
then A10: f | [.x1,x2.] is continuous by A6, FCONT_1:17;
f is_differentiable_on Z by A1, A6, A7, FDIFF_1:34, XBOOLE_1:1;
then consider x0 being Real such that
A11: ( x0 in ].x1,x2.[ & diff f,x0 = ((f . x2) - (f . x1)) / (x2 - x1) ) by A5, A10, Th3, A0, A6, XBOOLE_1:1;
0 = (f . x2) - (f . x1) by A2, A8, A9, A11, XCMPLX_1:6;
hence f . x1 = f . x2 ; :: thesis: verum

end;

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

reconsider Z = ].x2,x1.[ as open Subset of REAL ;
A13: [.x2,x1.] c= ].p,g.[ by A3, XXREAL_2:def 12;
A14: Z c= [.x2,x1.] by XXREAL_1:25;
then A15: Z c= ].p,g.[ by A13, XBOOLE_1:1;
0 <> x1 - x2 by A12;
then A16: 0 <> (x1 - x2) " by XCMPLX_1:203;
f | ].p,g.[ is continuous by A1, FDIFF_1:33;
then A17: f | [.x2,x1.] is continuous by A13, FCONT_1:17;
f is_differentiable_on Z by A1, A13, A14, FDIFF_1:34, XBOOLE_1:1;
then consider x0 being Real such that
A18: ( x0 in ].x2,x1.[ & diff f,x0 = ((f . x1) - (f . x2)) / (x1 - x2) ) by A12, A17, Th3, A0, A13, XBOOLE_1:1;
0 = (f . x1) - (f . x2) by A2, A15, A16, A18, XCMPLX_1:6;
hence f . x1 = f . x2 ; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

hence f | ].p,g.[ is V8() by PARTFUN2:77; :: thesis: verum