let f be PartFunc of REAL,REAL; :: thesis:
let a, b be Real; :: thesis:
assume A1: f is_right_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,a,x) ) & ( Intf is_left_convergent_in b or Intf is_left_divergent_to+infty_in b or Intf is_left_divergent_to-infty_in b ) ) ;

per cases by A2;

suppose A3: Intf is_left_convergent_in b ; :: thesis:

then A4: f is_right_ext_Riemann_integrable_on a,b by A1, A2, INTEGR10:def 1;
right_improper_integral (f,a,b) = lim_left (Intf,b) by A1, A2, A3, Def4
.= ext_right_integral (f,a,b) by A2, A3, A4, INTEGR10:def 3 ;
hence ( ( f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = ext_right_integral (f,a,b) ) or ( not f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = +infty ) or ( not f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = -infty ) ) by A3, A1, A2, INTEGR10:def 1; :: thesis:

end;

suppose A5: Intf is_left_divergent_to+infty_in b ; :: 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,a,x) ) holds
not I is_left_convergent_in b

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,a,x) ; :: thesis:

now :: thesis:

let x be Element of REAL ; :: thesis:
assume A8: x in dom Intf ; :: thesis:
then Intf . x = integral (f,a,x) 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_left_convergent_in b by A5, Th6; :: thesis:

end;

hence ( ( f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = ext_right_integral (f,a,b) ) or ( not f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = +infty ) or ( not f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = -infty ) ) by A1, Def4, INTEGR10:def 1; :: thesis:

end;

suppose A9: Intf is_left_divergent_to-infty_in b ; :: 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,a,x) ) holds
not I is_left_convergent_in b

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,a,x) ; :: thesis:

now :: thesis:

let x be Element of REAL ; :: thesis:
assume A12: x in dom Intf ; :: thesis:
then Intf . x = integral (f,a,x) 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_left_convergent_in b by A9, Th7; :: thesis:

end;

hence ( ( f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = ext_right_integral (f,a,b) ) or ( not f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = +infty ) or ( not f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = -infty ) ) by A1, Def4, INTEGR10:def 1; :: thesis:

end;

end;