theorem Th26: :: INTEGR26:26

for a, b being Real
for f being PartFunc of REAL,REAL st a < b & [.a,b.] c= dom f & f | [.a,b.] is continuous 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_on ].a,b.[ & F `| ].a,b.[ = f | ].a,b.[ )