theorem Th1955: :: ORDEQ_02:13

for a, b, x0 being Real
for X being RealBanachSpace
for F being PartFunc of REAL, the carrier of X
for f being continuous PartFunc of REAL, the carrier of X st [.a,b.] c= dom f & ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds
F /. x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds
( F is_differentiable_in x0 & diff (F,x0) = f /. x0 )