let X be RealBanachSpace; :: thesis: for a, b being Real

for f being PartFunc of REAL, the carrier of X st [.a,b.] c= dom f & ( for x being Real st x in [.a,b.] holds

f is_continuous_in x ) & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds

diff (f,x) = 0. X ) holds

f | ].a,b.[ is constant

let a, b be Real; :: thesis: for f being PartFunc of REAL, the carrier of X st [.a,b.] c= dom f & ( for x being Real st x in [.a,b.] holds

f is_continuous_in x ) & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds

diff (f,x) = 0. X ) holds

f | ].a,b.[ is constant

let f be PartFunc of REAL, the carrier of X; :: thesis: ( [.a,b.] c= dom f & ( for x being Real st x in [.a,b.] holds

f is_continuous_in x ) & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds

diff (f,x) = 0. X ) implies f | ].a,b.[ is constant )

assume that

A1: ( [.a,b.] c= dom f & ( for x being Real st x in [.a,b.] holds

f is_continuous_in x ) ) and

A2: ( f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds

diff (f,x) = 0. X ) ) ; :: thesis: f | ].a,b.[ is constant

for f being PartFunc of REAL, the carrier of X st [.a,b.] c= dom f & ( for x being Real st x in [.a,b.] holds

f is_continuous_in x ) & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds

diff (f,x) = 0. X ) holds

f | ].a,b.[ is constant

let a, b be Real; :: thesis: for f being PartFunc of REAL, the carrier of X st [.a,b.] c= dom f & ( for x being Real st x in [.a,b.] holds

f is_continuous_in x ) & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds

diff (f,x) = 0. X ) holds

f | ].a,b.[ is constant

let f be PartFunc of REAL, the carrier of X; :: thesis: ( [.a,b.] c= dom f & ( for x being Real st x in [.a,b.] holds

f is_continuous_in x ) & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds

diff (f,x) = 0. X ) implies f | ].a,b.[ is constant )

assume that

A1: ( [.a,b.] c= dom f & ( for x being Real st x in [.a,b.] holds

f is_continuous_in x ) ) and

A2: ( f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds

diff (f,x) = 0. X ) ) ; :: thesis: f | ].a,b.[ is constant

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

f /. x1 = f /. x2

hence
f | ].a,b.[ is constant
by PARTFUN2:36; :: thesis: verumf /. x1 = f /. x2

let x1, x2 be Element of REAL ; :: thesis: ( x1 in ].a,b.[ /\ (dom f) & x2 in ].a,b.[ /\ (dom f) implies f /. x1 = f /. x2 )

assume ( x1 in ].a,b.[ /\ (dom f) & x2 in ].a,b.[ /\ (dom f) ) ; :: thesis: f /. x1 = f /. x2

then A4: ( x1 in ].a,b.[ & x2 in ].a,b.[ ) by XBOOLE_0:def 4;

reconsider Z1 = ].x1,x2.[, Z2 = ].x2,x1.[ as open Subset of REAL ;

A7: ( ].a,b.[ c= [.a,b.] & Z1 c= [.x1,x2.] & Z2 c= [.x2,x1.] ) by XXREAL_1:25;

then ( [.x1,x2.] c= [.a,b.] & [.x2,x1.] c= [.a,b.] ) by A4, XXREAL_2:def 12;

then C1: ( [.x1,x2.] c= dom f & [.x2,x1.] c= dom f & ( for x being Real st x in [.x1,x2.] holds

f is_continuous_in x ) & ( for x being Real st x in [.x2,x1.] holds

f is_continuous_in x ) ) by A1;

( [.x1,x2.] c= ].a,b.[ & [.x2,x1.] c= ].a,b.[ ) by A4, XXREAL_2:def 12;

then ( f is_differentiable_on Z1 & ( for x being Real st x in Z1 holds

diff (f,x) = 0. X ) & f is_differentiable_on Z2 & ( for x being Real st x in Z2 holds

diff (f,x) = 0. X ) ) by A2, A7, NDIFF_3:24, XBOOLE_1:1;

then ( ( x1 < x2 implies f /. x1 = f /. x2 ) & ( x2 < x1 implies f /. x1 = f /. x2 ) ) by C1, Th45a;

hence f /. x1 = f /. x2 by XXREAL_0:1; :: thesis: verum

end;assume ( x1 in ].a,b.[ /\ (dom f) & x2 in ].a,b.[ /\ (dom f) ) ; :: thesis: f /. x1 = f /. x2

then A4: ( x1 in ].a,b.[ & x2 in ].a,b.[ ) by XBOOLE_0:def 4;

reconsider Z1 = ].x1,x2.[, Z2 = ].x2,x1.[ as open Subset of REAL ;

A7: ( ].a,b.[ c= [.a,b.] & Z1 c= [.x1,x2.] & Z2 c= [.x2,x1.] ) by XXREAL_1:25;

then ( [.x1,x2.] c= [.a,b.] & [.x2,x1.] c= [.a,b.] ) by A4, XXREAL_2:def 12;

then C1: ( [.x1,x2.] c= dom f & [.x2,x1.] c= dom f & ( for x being Real st x in [.x1,x2.] holds

f is_continuous_in x ) & ( for x being Real st x in [.x2,x1.] holds

f is_continuous_in x ) ) by A1;

( [.x1,x2.] c= ].a,b.[ & [.x2,x1.] c= ].a,b.[ ) by A4, XXREAL_2:def 12;

then ( f is_differentiable_on Z1 & ( for x being Real st x in Z1 holds

diff (f,x) = 0. X ) & f is_differentiable_on Z2 & ( for x being Real st x in Z2 holds

diff (f,x) = 0. X ) ) by A2, A7, NDIFF_3:24, XBOOLE_1:1;

then ( ( x1 < x2 implies f /. x1 = f /. x2 ) & ( x2 < x1 implies f /. x1 = f /. x2 ) ) by C1, Th45a;

hence f /. x1 = f /. x2 by XXREAL_0:1; :: thesis: verum