let f be PartFunc of REAL,REAL; :: thesis: for a being Real st f is_+infty_improper_integrable_on a & improper_integral_+infty (f,a) = +infty holds
for Intf being PartFunc of REAL,REAL st dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) holds
Intf is divergent_in+infty_to+infty
let a be Real; :: thesis: ( f is_+infty_improper_integrable_on a & improper_integral_+infty (f,a) = +infty implies for Intf being PartFunc of REAL,REAL st dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) holds
Intf is divergent_in+infty_to+infty )
assume that
A1: f is_+infty_improper_integrable_on a and
A2: improper_integral_+infty (f,a) = +infty ; :: thesis: for Intf being PartFunc of REAL,REAL st dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) holds
Intf is divergent_in+infty_to+infty
let Intf be PartFunc of REAL,REAL; :: thesis: ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) implies Intf is divergent_in+infty_to+infty )
assume that
A3: dom Intf = right_closed_halfline a and
A4: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ; :: thesis: Intf is divergent_in+infty_to+infty
consider I being PartFunc of REAL,REAL such that
A5: ( dom I = right_closed_halfline a & ( for x being Real st x in dom I holds
I . x = integral (f,a,x) ) & ( ( I is convergent_in+infty & improper_integral_+infty (f,a) = lim_in+infty I ) or ( I is divergent_in+infty_to+infty & improper_integral_+infty (f,a) = +infty ) or ( I is divergent_in+infty_to-infty & improper_integral_+infty (f,a) = -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 divergent_in+infty_to+infty by A2, A3, A5, PARTFUN1:5; :: thesis: verum