let f be PartFunc of REAL,REAL; :: thesis:
let b be Real; :: thesis:
assume A1: f is_+infty_improper_integrable_on b ; :: thesis:
then consider Intf being PartFunc of REAL,REAL such that
A2: dom Intf = right_closed_halfline b and
A3: for x being Real st x in dom Intf holds
Intf . x = integral (f,b,x) and
A4: ( Intf is convergent_in+infty or Intf is divergent_in+infty_to+infty or Intf is divergent_in+infty_to-infty ) ;

per cases by A4;

suppose A5: Intf is convergent_in+infty ; :: thesis:

then A6: f is_+infty_ext_Riemann_integrable_on b by A1, A2, A3, INTEGR10:def 5;
improper_integral_+infty (f,b) = lim_in+infty Intf by A1, A2, A3, A5, Def4
.= infty_ext_right_integral (f,b) by A6, A2, A3, A5, INTEGR10:def 7 ;
hence ( ( f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ) or ( not f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty (f,b) = +infty ) or ( not f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty (f,b) = -infty ) ) by A5, A1, A2, A3, INTEGR10:def 5; :: thesis:

end;

suppose A7: Intf is divergent_in+infty_to+infty ; :: thesis:

for I being PartFunc of REAL,REAL st dom I = right_closed_halfline b & ( for x being Real st x in dom I holds
I . x = integral (f,b,x) ) holds
not I is convergent_in+infty

proof

let I be PartFunc of REAL,REAL; :: thesis:
assume that
A8: dom I = right_closed_halfline b and
A9: for x being Real st x in dom I holds
I . x = integral (f,b,x) ; :: thesis:

now :: thesis:

let x be Element of REAL ; :: thesis:
assume A10: x in dom Intf ; :: thesis:
then Intf . x = integral (f,b,x) by A3;
hence Intf . x = I . x by A2, A8, A9, A10; :: thesis:

end;

then Intf = I by A2, A8, PARTFUN1:5;
hence not I is convergent_in+infty by A7, Th3; :: thesis:

end;

hence ( ( f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ) or ( not f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty (f,b) = +infty ) or ( not f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty (f,b) = -infty ) ) by A1, Def4, INTEGR10:def 5; :: thesis:

end;

suppose A11: Intf is divergent_in+infty_to-infty ; :: thesis:

for I being PartFunc of REAL,REAL st dom I = right_closed_halfline b & ( for x being Real st x in dom I holds
I . x = integral (f,b,x) ) holds
not I is convergent_in+infty

proof

let I be PartFunc of REAL,REAL; :: thesis:
assume that
A12: dom I = right_closed_halfline b and
A13: for x being Real st x in dom I holds
I . x = integral (f,b,x) ; :: thesis:

now :: thesis:

let x be Element of REAL ; :: thesis:
assume A14: x in dom Intf ; :: thesis:
then Intf . x = integral (f,b,x) by A3;
hence Intf . x = I . x by A2, A12, A13, A14; :: thesis:

end;

then Intf = I by A2, A12, PARTFUN1:5;
hence not I is convergent_in+infty by A11, Th4; :: thesis:

end;

hence ( ( f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ) or ( not f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty (f,b) = +infty ) or ( not f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty (f,b) = -infty ) ) by A1, Def4, INTEGR10:def 5; :: thesis:

end;

end;