theorem Th20: :: INTEGRA7:20

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