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

for f being PartFunc of REAL, the carrier of X st a <= b & [.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 /. b = f /. a

let a, b be Real; :: thesis: for f being PartFunc of REAL, the carrier of X st a <= b & [.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 /. b = f /. a

let f be PartFunc of REAL, the carrier of X; :: thesis: ( a <= b & [.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 /. b = f /. a )

assume that

A1: ( a <= b & [.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.[ and

A3: for x being Real st x in ].a,b.[ holds

diff (f,x) = 0. X ; :: thesis: f /. b = f /. a

A5: for x being Real st x in ].a,b.[ holds

f is_differentiable_in x by A2, NDIFF_3:10;

then ||.((f /. b) - (f /. a)).|| = 0 ;

hence f /. b = f /. a by NORMSP_1:6; :: thesis: verum

for f being PartFunc of REAL, the carrier of X st a <= b & [.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 /. b = f /. a

let a, b be Real; :: thesis: for f being PartFunc of REAL, the carrier of X st a <= b & [.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 /. b = f /. a

let f be PartFunc of REAL, the carrier of X; :: thesis: ( a <= b & [.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 /. b = f /. a )

assume that

A1: ( a <= b & [.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.[ and

A3: for x being Real st x in ].a,b.[ holds

diff (f,x) = 0. X ; :: thesis: f /. b = f /. a

A5: for x being Real st x in ].a,b.[ holds

f is_differentiable_in x by A2, NDIFF_3:10;

now :: thesis: for x being Real st x in ].a,b.[ holds

||.(diff (f,x)).|| <= 0

then
||.((f /. b) - (f /. a)).|| <= 0 * |.(b - a).|
by A5, Th519, A1;||.(diff (f,x)).|| <= 0

let x be Real; :: thesis: ( x in ].a,b.[ implies ||.(diff (f,x)).|| <= 0 )

assume x in ].a,b.[ ; :: thesis: ||.(diff (f,x)).|| <= 0

then ||.(diff (f,x)).|| = ||.(0. X).|| by A3;

hence ||.(diff (f,x)).|| <= 0 ; :: thesis: verum

end;assume x in ].a,b.[ ; :: thesis: ||.(diff (f,x)).|| <= 0

then ||.(diff (f,x)).|| = ||.(0. X).|| by A3;

hence ||.(diff (f,x)).|| <= 0 ; :: thesis: verum

then ||.((f /. b) - (f /. a)).|| = 0 ;

hence f /. b = f /. a by NORMSP_1:6; :: thesis: verum