let a, b be Real; :: thesis: for f being PartFunc of REAL,REAL st a < b & [.a,b.] c= dom f & f | [.a,b.] is continuous holds
ex F being PartFunc of REAL,REAL st
( F is_antiderivative_of f,['a,b'] & ( for x being Real st x in [.a,b.] holds
F . x = integral (f,a,x) ) )
let f be PartFunc of REAL,REAL; :: thesis: ( a < b & [.a,b.] c= dom f & f | [.a,b.] is continuous implies ex F being PartFunc of REAL,REAL st
( F is_antiderivative_of f,['a,b'] & ( for x being Real st x in [.a,b.] holds
F . x = integral (f,a,x) ) ) )
assume that
A1: a < b and
A2: [.a,b.] c= dom f and
A3: f | [.a,b.] is continuous ; :: thesis: ex F being PartFunc of REAL,REAL st
( F is_antiderivative_of f,['a,b'] & ( for x being Real st x in [.a,b.] holds
F . x = integral (f,a,x) ) )
reconsider I = ['a,b'] as non empty Interval ;
A4: I = [.a,b.] by A1, INTEGRA5:def 3;
consider F being PartFunc of REAL,REAL such that
A5: ( dom F = REAL & ( for x being Real st x in I holds
F . x = integral (f,a,x) ) ) by Lm1;
( F is_differentiable_on_interval I & F `\ I = f | I ) by A1, A2, A3, A5, A4, Th37;
hence ex F being PartFunc of REAL,REAL st
( F is_antiderivative_of f,['a,b'] & ( for x being Real st x in [.a,b.] holds
F . x = integral (f,a,x) ) ) by Def1, A5, A4; :: thesis: verum