consider Intf being PartFunc of REAL,REAL such that
A2: dom Intf = ].a,b.] and
A3: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
A4: ( Intf is_right_convergent_in a or Intf is_right_divergent_to+infty_in a or Intf is_right_divergent_to-infty_in a ) by A1;

per cases ( Intf is_right_convergent_in a or Intf is_right_divergent_to+infty_in a or Intf is_right_divergent_to-infty_in a ) by A4;

suppose A5: Intf is_right_convergent_in a ; :: thesis: ex b₁ being ExtReal ex 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) ) & ( ( Intf is_right_convergent_in a & b₁ = lim_right (Intf,a) ) or ( Intf is_right_divergent_to+infty_in a & b₁ = +infty ) or ( Intf is_right_divergent_to-infty_in a & b₁ = -infty ) ) )

reconsider IT = lim_right (Intf,a) as ExtReal ;
take IT ; :: thesis: ex 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) ) & ( ( Intf is_right_convergent_in a & IT = lim_right (Intf,a) ) or ( Intf is_right_divergent_to+infty_in a & IT = +infty ) or ( Intf is_right_divergent_to-infty_in a & IT = -infty ) ) )
thus ex 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) ) & ( ( Intf is_right_convergent_in a & IT = lim_right (Intf,a) ) or ( Intf is_right_divergent_to+infty_in a & IT = +infty ) or ( Intf is_right_divergent_to-infty_in a & IT = -infty ) ) ) by A2, A3, A5; :: thesis: verum

end;

suppose A6: Intf is_right_divergent_to+infty_in a ; :: thesis: ex b₁ being ExtReal ex 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) ) & ( ( Intf is_right_convergent_in a & b₁ = lim_right (Intf,a) ) or ( Intf is_right_divergent_to+infty_in a & b₁ = +infty ) or ( Intf is_right_divergent_to-infty_in a & b₁ = -infty ) ) )

take +infty ; :: thesis: ex 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) ) & ( ( Intf is_right_convergent_in a & +infty = lim_right (Intf,a) ) or ( Intf is_right_divergent_to+infty_in a & +infty = +infty ) or ( Intf is_right_divergent_to-infty_in a & +infty = -infty ) ) )
thus ex 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) ) & ( ( Intf is_right_convergent_in a & +infty = lim_right (Intf,a) ) or ( Intf is_right_divergent_to+infty_in a & +infty = +infty ) or ( Intf is_right_divergent_to-infty_in a & +infty = -infty ) ) ) by A2, A3, A6; :: thesis: verum

end;

suppose A7: Intf is_right_divergent_to-infty_in a ; :: thesis: ex b₁ being ExtReal ex 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) ) & ( ( Intf is_right_convergent_in a & b₁ = lim_right (Intf,a) ) or ( Intf is_right_divergent_to+infty_in a & b₁ = +infty ) or ( Intf is_right_divergent_to-infty_in a & b₁ = -infty ) ) )

take -infty ; :: thesis: ex 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) ) & ( ( Intf is_right_convergent_in a & -infty = lim_right (Intf,a) ) or ( Intf is_right_divergent_to+infty_in a & -infty = +infty ) or ( Intf is_right_divergent_to-infty_in a & -infty = -infty ) ) )
thus ex 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) ) & ( ( Intf is_right_convergent_in a & -infty = lim_right (Intf,a) ) or ( Intf is_right_divergent_to+infty_in a & -infty = +infty ) or ( Intf is_right_divergent_to-infty_in a & -infty = -infty ) ) ) by A2, A3, A7; :: thesis: verum

end;

end;