let f be PartFunc of REAL,REAL; :: thesis:
let a, b be Real; :: thesis:
assume A1: f is_left_improper_integrable_on a,b ; :: thesis:
then consider Intf being PartFunc of REAL,REAL such that
A2: ( 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 or Intf is_right_divergent_to+infty_in a or Intf is_right_divergent_to-infty_in a ) ) ;

per cases by A2;

suppose A3: Intf is_right_convergent_in a ; :: thesis:

then A4: f is_left_ext_Riemann_integrable_on a,b by A1, A2, INTEGR10:def 2;
left_improper_integral (f,a,b) = lim_right (Intf,a) by A1, A2, A3, Def3
.= ext_left_integral (f,a,b) by A2, A3, A4, INTEGR10:def 4 ;
hence ( ( f is_left_ext_Riemann_integrable_on a,b & left_improper_integral (f,a,b) = ext_left_integral (f,a,b) ) or ( not f is_left_ext_Riemann_integrable_on a,b & left_improper_integral (f,a,b) = +infty ) or ( not f is_left_ext_Riemann_integrable_on a,b & left_improper_integral (f,a,b) = -infty ) ) by A1, A2, A3, INTEGR10:def 2; :: thesis:

end;

suppose A5: Intf is_right_divergent_to+infty_in a ; :: thesis:

for I being PartFunc of REAL,REAL st dom I = ].a,b.] & ( for x being Real st x in dom I holds
I . x = integral (f,x,b) ) holds
not I is_right_convergent_in a

proof

let I be PartFunc of REAL,REAL; :: thesis:
assume that
A6: dom I = ].a,b.] and
A7: 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 A8: x in dom Intf ; :: thesis:
then Intf . x = integral (f,x,b) by A2;
hence Intf . x = I . x by A2, A6, A7, A8; :: thesis:

end;

then Intf = I by A2, A6, PARTFUN1:5;
hence not I is_right_convergent_in a by A5, Th8; :: thesis:

end;

hence ( ( f is_left_ext_Riemann_integrable_on a,b & left_improper_integral (f,a,b) = ext_left_integral (f,a,b) ) or ( not f is_left_ext_Riemann_integrable_on a,b & left_improper_integral (f,a,b) = +infty ) or ( not f is_left_ext_Riemann_integrable_on a,b & left_improper_integral (f,a,b) = -infty ) ) by A1, Def3, INTEGR10:def 2; :: thesis:

end;

suppose A9: Intf is_right_divergent_to-infty_in a ; :: thesis:

for I being PartFunc of REAL,REAL st dom I = ].a,b.] & ( for x being Real st x in dom I holds
I . x = integral (f,x,b) ) holds
not I is_right_convergent_in a

proof

let I be PartFunc of REAL,REAL; :: thesis:
assume that
A10: dom I = ].a,b.] and
A11: 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 A12: x in dom Intf ; :: thesis:
then Intf . x = integral (f,x,b) by A2;
hence Intf . x = I . x by A2, A10, A11, A12; :: thesis:

end;

then Intf = I by A2, A10, PARTFUN1:5;
hence not I is_right_convergent_in a by A9, Th9; :: thesis:

end;

hence ( ( f is_left_ext_Riemann_integrable_on a,b & left_improper_integral (f,a,b) = ext_left_integral (f,a,b) ) or ( not f is_left_ext_Riemann_integrable_on a,b & left_improper_integral (f,a,b) = +infty ) or ( not f is_left_ext_Riemann_integrable_on a,b & left_improper_integral (f,a,b) = -infty ) ) by A1, Def3, INTEGR10:def 2; :: thesis:

end;

end;