let a, b be Real; :: thesis: 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)
let X be set ; :: thesis: 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)
let f, F be PartFunc of REAL,REAL; :: thesis: ( a <= b & ['a,b'] c= X & F is_integral_of f,X & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded implies F . b = (integral (f,a,b)) + (F . a) )
assume that
A1: a <= b and
A2: ['a,b'] c= X ; :: thesis: ( not F is_integral_of f,X or not f is_integrable_on ['a,b'] or not f | ['a,b'] is bounded or F . b = (integral (f,a,b)) + (F . a) )
assume A3: F is_integral_of f,X ; :: thesis: ( not f is_integrable_on ['a,b'] or not f | ['a,b'] is bounded or F . b = (integral (f,a,b)) + (F . a) )
then A4: ( F is_differentiable_on X & F `| X = f | X ) by Lm1;
assume f is_integrable_on ['a,b'] ; :: thesis: ( not f | ['a,b'] is bounded or F . b = (integral (f,a,b)) + (F . a) )
then A5: f || ['a,b'] is integrable ;
assume A6: f | ['a,b'] is bounded ; :: thesis: F . b = (integral (f,a,b)) + (F . a)
(F `| X) || ['a,b'] = (f | X) | ['a,b'] by A3, Lm1;
then A7: (F `| X) || ['a,b'] = f || ['a,b'] by A2, FUNCT_1:51;
then F `| X is_integrable_on ['a,b'] by A5;
then F . b = (integral ((f | X),a,b)) + (F . a) by A1, A2, A4, A7, A6, Th10;
then F . b = (integral ((f | X),['a,b'])) + (F . a) by A1, INTEGRA5:def 4;
then F . b = (integral (f,['a,b'])) + (F . a) by A2, FUNCT_1:51;
hence F . b = (integral (f,a,b)) + (F . a) by A1, INTEGRA5:def 4; :: thesis: verum