let f be PartFunc of REAL,REAL; 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; ( 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
; 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; ( 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)
; 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
hence
Intf is_left_divergent_to+infty_in b
by A2, A3, A5, PARTFUN1:5; verum