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 ) by A1;

per cases by A4;

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

reconsider IT = lim_in-infty Intf as ExtReal ;
take IT ; :: thesis:
thus ex Intf being PartFunc of REAL,REAL st
( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) & ( ( Intf is convergent_in-infty & IT = lim_in-infty Intf ) or ( Intf is divergent_in-infty_to+infty & IT = +infty ) or ( Intf is divergent_in-infty_to-infty & IT = -infty ) ) ) by A2, A3, A5; :: thesis:

end;

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

take +infty ; :: thesis:
thus ex Intf being PartFunc of REAL,REAL st
( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) & ( ( Intf is convergent_in-infty & +infty = lim_in-infty Intf ) or ( Intf is divergent_in-infty_to+infty & +infty = +infty ) or ( Intf is divergent_in-infty_to-infty & +infty = -infty ) ) ) by A2, A3, A6; :: thesis:

end;

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

take -infty ; :: thesis:
thus ex Intf being PartFunc of REAL,REAL st
( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) & ( ( Intf is convergent_in-infty & -infty = lim_in-infty Intf ) or ( Intf is divergent_in-infty_to+infty & -infty = +infty ) or ( Intf is divergent_in-infty_to-infty & -infty = -infty ) ) ) by A2, A3, A7; :: thesis:

end;

end;