theorem Th32: :: INTEGRA7:32

for a, b being Real
for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is continuous holds
ex F being PartFunc of REAL,REAL st
( ].a,b.[ c= dom F & ( for t being Real st t in ].a,b.[ holds
F . t = integral (f,a,t) ) & ( for t being Real st t in ].a,b.[ holds
( F is_differentiable_in t & diff (F,t) = f . t ) ) )