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 & X c= dom f & f | X is continuous & F is_integral_of f,X 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 & X c= dom f & f | X is continuous & F is_integral_of f,X holds
F . b = (integral (f,a,b)) + (F . a)
let f, F be PartFunc of REAL,REAL; :: thesis: ( a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous & F is_integral_of f,X implies F . b = (integral (f,a,b)) + (F . a) )
assume that
A1: a <= b and
A2: [.a,b.] c= X and
A3: X c= dom f ; :: thesis: ( not f | X is continuous or not F is_integral_of f,X or F . b = (integral (f,a,b)) + (F . a) )
assume f | X is continuous ; :: thesis: ( not F is_integral_of f,X or F . b = (integral (f,a,b)) + (F . a) )
then A4: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A1, A2, A3, Th19;
A5: [.a,b.] = ['a,b'] by A1, INTEGRA5:def 3;
assume F is_integral_of f,X ; :: thesis: F . b = (integral (f,a,b)) + (F . a)
hence F . b = (integral (f,a,b)) + (F . a) by A1, A2, A5, A4, Th18; :: thesis: verum