theorem Th34: :: ORDEQ_01:34

for n being non zero Element of NAT
for a, b being Real
for f being continuous PartFunc of REAL,(REAL-NS n)
for F being PartFunc of REAL,(REAL-NS n) st a <= b & 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