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 = left_closed_halfline b and
A3: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) 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 6;
improper_integral_-infty (f,b) = lim_in-infty Intf by A1, A2, A3, A5, Def3
.= infty_ext_left_integral (f,b) by A6, A2, A3, A5, INTEGR10:def 8 ;
hence ( ( f is_-infty_ext_Riemann_integrable_on b & improper_integral_-infty (f,b) = infty_ext_left_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 6; :: thesis:

end;

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

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

proof

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

now :: thesis:

let x be Element of REAL ; :: thesis:
assume A10: x in dom Intf ; :: thesis:
then Intf . x = integral (f,x,b) 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, Th1; :: thesis:

end;

hence ( ( f is_-infty_ext_Riemann_integrable_on b & improper_integral_-infty (f,b) = infty_ext_left_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, Def3, INTEGR10:def 6; :: thesis:

end;

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

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

proof

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

now :: thesis:

let x be Element of REAL ; :: thesis:
assume A14: x in dom Intf ; :: thesis:
then Intf . x = integral (f,x,b) 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, Th2; :: thesis:

end;

hence ( ( f is_-infty_ext_Riemann_integrable_on b & improper_integral_-infty (f,b) = infty_ext_left_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, Def3, INTEGR10:def 6; :: thesis:

end;

end;