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,a,x) and
A4: ( Intf is_left_convergent_in b or Intf is_left_divergent_to+infty_in b or Intf is_left_divergent_to-infty_in b ) by A1;

per cases ( Intf is_left_convergent_in b or Intf is_left_divergent_to+infty_in b or Intf is_left_divergent_to-infty_in b ) by A4;

suppose A5: Intf is_left_convergent_in b ; :: 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,a,x) ) & ( ( Intf is_left_convergent_in b & b₁ = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & b₁ = +infty ) or ( Intf is_left_divergent_to-infty_in b & b₁ = -infty ) ) )

reconsider IT = lim_left (Intf,b) 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,a,x) ) & ( ( Intf is_left_convergent_in b & IT = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & IT = +infty ) or ( Intf is_left_divergent_to-infty_in b & 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,a,x) ) & ( ( Intf is_left_convergent_in b & IT = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & IT = +infty ) or ( Intf is_left_divergent_to-infty_in b & IT = -infty ) ) ) by A2, A3, A5; :: thesis: verum

end;

suppose A6: Intf is_left_divergent_to+infty_in b ; :: 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,a,x) ) & ( ( Intf is_left_convergent_in b & b₁ = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & b₁ = +infty ) or ( Intf is_left_divergent_to-infty_in b & 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,a,x) ) & ( ( Intf is_left_convergent_in b & +infty = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & +infty = +infty ) or ( Intf is_left_divergent_to-infty_in b & +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,a,x) ) & ( ( Intf is_left_convergent_in b & +infty = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & +infty = +infty ) or ( Intf is_left_divergent_to-infty_in b & +infty = -infty ) ) ) by A2, A3, A6; :: thesis: verum

end;

suppose A7: Intf is_left_divergent_to-infty_in b ; :: 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,a,x) ) & ( ( Intf is_left_convergent_in b & b₁ = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & b₁ = +infty ) or ( Intf is_left_divergent_to-infty_in b & 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,a,x) ) & ( ( Intf is_left_convergent_in b & -infty = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & -infty = +infty ) or ( Intf is_left_divergent_to-infty_in b & -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,a,x) ) & ( ( Intf is_left_convergent_in b & -infty = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & -infty = +infty ) or ( Intf is_left_divergent_to-infty_in b & -infty = -infty ) ) ) by A2, A3, A7; :: thesis: verum

end;

end;