theorem :: INTEGRA6:29

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