let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st f is_left_improper_integrable_on a,b & left_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,x,b) ) holds
Intf is_right_divergent_to+infty_in a
let a, b be Real; :: thesis: ( f is_left_improper_integrable_on a,b & left_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,x,b) ) holds
Intf is_right_divergent_to+infty_in a )
assume that
A1: f is_left_improper_integrable_on a,b and
A2: left_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,x,b) ) holds
Intf is_right_divergent_to+infty_in a
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,x,b) ) implies Intf is_right_divergent_to+infty_in a )
assume that
A3: dom Intf = ].a,b.] and
A4: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ; :: thesis: Intf is_right_divergent_to+infty_in a
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,x,b) ) & ( ( I is_right_convergent_in a & left_improper_integral (f,a,b) = lim_right (I,a) ) or ( I is_right_divergent_to+infty_in a & left_improper_integral (f,a,b) = +infty ) or ( I is_right_divergent_to-infty_in a & left_improper_integral (f,a,b) = -infty ) ) ) by A1, Def3;
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,x,b) & Intf . x = integral (f,x,b) ) by A3, A4, A5;
hence I . x = Intf . x ; :: thesis: verum

end;

hence Intf is_right_divergent_to+infty_in a by A2, A3, A5, PARTFUN1:5; :: thesis: verum