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