let a, b be Real; 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 ; 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; ( 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
; ( 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
; ( 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
; F . b = (integral (f,a,b)) + (F . a)
hence
F . b = (integral (f,a,b)) + (F . a)
by A1, A2, A5, A4, Th18; verum