consider Intf being PartFunc of REAL,REAL such that
A2: dom Intf = right_closed_halfline a and
A3: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) 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 = right_closed_halfline a & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) & ( ( 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 = right_closed_halfline a & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) & ( ( 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 = right_closed_halfline a & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) & ( ( 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;