theorem Th18: :: INTEGRA7:18

for a, b being Real
for X being set
for f, F being PartFunc of REAL,REAL st a <= b & ['a,b'] c= X & F is_integral_of f,X & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds
F . b = (integral (f,a,b)) + (F . a)