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
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
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;
hence f | ].a,b.[ is constant by PARTFUN2:36; :: thesis: verum