let a, b be real number ; :: thesis: 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)
let X be set ; :: thesis: 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)
let F be PartFunc of REAL , REAL ; :: thesis: ( a <= b & ['a,b'] c= X & F is_differentiable_on X & F `| X is_integrable_on ['a,b'] & (F `| X) | ['a,b'] is bounded implies F . b = (integral (F `| X),a,b) + (F . a) )
assume that
A1: a <= b and
A2: ( ['a,b'] c= X & F is_differentiable_on X & F `| X is_integrable_on ['a,b'] & (F `| X) | ['a,b'] is bounded ) ; :: thesis: F . b = (integral (F `| X),a,b) + (F . a)
A3: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 4;
then [.a,b.] = [.(lower_bound [.a,b.]),(upper_bound [.a,b.]).] by INTEGRA1:5;
then A4: ( a = lower_bound [.a,b.] & b = upper_bound [.a,b.] ) by A3, INTEGRA1:6;
integral (F `| X),a,b = integral (F `| X),['a,b'] by A1, INTEGRA5:def 5;
then integral (F `| X),a,b = (F . (upper_bound ['a,b'])) - (F . (lower_bound ['a,b'])) by A2, INTEGRA5:13;
hence F . b = (integral (F `| X),a,b) + (F . a) by A3, A4; :: thesis: verum