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;
now :: thesis: for x being Real st x in ].a,b.[ holds
||.(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;
then ||.((f /. b) - (f /. a)).|| <= 0 * |.(b - a).| by A5, Th519, A1;
then ||.((f /. b) - (f /. a)).|| = 0 ;
hence f /. b = f /. a by NORMSP_1:6; :: thesis: verum