let a, b be real number ; :: 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;
(F `| X) || ['a,b'] = (f | X) | ['a,b'] by A3, Lm1;
then A5: (F `| X) || ['a,b'] = f || ['a,b'] by A2, FUNCT_1:82;
assume f is_integrable_on ['a,b'] ; :: thesis: ( not f | ['a,b'] is bounded or F . b = (integral f,a,b) + (F . a) )
then f || ['a,b'] is integrable by INTEGRA5:def 2;
then A6: F `| X is_integrable_on ['a,b'] by A5, INTEGRA5:def 2;
assume f | ['a,b'] is bounded ; :: thesis: F . b = (integral f,a,b) + (F . a)
then ((F `| X) | ['a,b']) | ['a,b'] is bounded by A5, INTEGRA5:9;
then F . b = (integral (f | X),a,b) + (F . a) by A1, A2, A4, A6, Th3, Th10;
then F . b = (integral (f | X),['a,b']) + (F . a) by A1, INTEGRA5:def 5;
then F . b = (integral f,['a,b']) + (F . a) by A2, FUNCT_1:82;
hence F . b = (integral f,a,b) + (F . a) by A1, INTEGRA5:def 5; :: thesis: verum