let a, b be Real; :: 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)
integral ((F `| X),a,b) = integral ((F `| X),['a,b']) by A1, INTEGRA5:def 4;
then A3: integral ((F `| X),a,b) = (F . (upper_bound ['a,b'])) - (F . (lower_bound ['a,b'])) by A2, INTEGRA5:13;
A4: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then A5: [.a,b.] = [.(lower_bound [.a,b.]),(upper_bound [.a,b.]).] by INTEGRA1:4;
then a = lower_bound [.a,b.] by A4, INTEGRA1:5;
hence F . b = (integral ((F `| X),a,b)) + (F . a) by A4, A5, A3, INTEGRA1:5; :: thesis: verum