theorem Th35: :: ORDEQ_02:14

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