for X being RealBanachSpace
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