theorem Th33: :: INTEGR26:33

for a, b being Real
for f, F being PartFunc of REAL,REAL st a <= b & [.a,b.] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & [.a,b.] = dom F & ( for x being Real st x in [.a,b.] holds
F . x = integral (f,a,x) ) holds
F is Lipschitzian