let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st f is_right_improper_integrable_on a,b & right_improper_integral (f,a,b) = +infty holds
for Intf being PartFunc of REAL,REAL st dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) holds
Intf is_left_divergent_to+infty_in b
let a, b be Real; :: thesis: ( f is_right_improper_integrable_on a,b & right_improper_integral (f,a,b) = +infty implies for Intf being PartFunc of REAL,REAL st dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) holds
Intf is_left_divergent_to+infty_in b )
assume that
A1: f is_right_improper_integrable_on a,b and
A2: right_improper_integral (f,a,b) = +infty ; :: thesis: for Intf being PartFunc of REAL,REAL st dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) holds
Intf is_left_divergent_to+infty_in b
let Intf be PartFunc of REAL,REAL; :: thesis: ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) implies Intf is_left_divergent_to+infty_in b )
assume that
A3: dom Intf = [.a,b.[ and
A4: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ; :: thesis: Intf is_left_divergent_to+infty_in b
consider I being PartFunc of REAL,REAL such that
A5: ( dom I = [.a,b.[ & ( for x being Real st x in dom I holds
I . x = integral (f,a,x) ) & ( ( I is_left_convergent_in b & right_improper_integral (f,a,b) = lim_left (I,b) ) or ( I is_left_divergent_to+infty_in b & right_improper_integral (f,a,b) = +infty ) or ( I is_left_divergent_to-infty_in b & right_improper_integral (f,a,b) = -infty ) ) ) by A1, Def4;
for x being Element of REAL st x in dom I holds
I . x = Intf . x

proof

let x be Element of REAL ; :: thesis: ( x in dom I implies I . x = Intf . x )
assume x in dom I ; :: thesis: I . x = Intf . x
then ( I . x = integral (f,a,x) & Intf . x = integral (f,a,x) ) by A3, A4, A5;
hence I . x = Intf . x ; :: thesis: verum

end;

hence Intf is_left_divergent_to+infty_in b by A2, A3, A5, PARTFUN1:5; :: thesis: verum