let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st 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_divergent_to+infty_in b or Intf is_left_divergent_to-infty_in b ) ) holds
not f is_right_ext_Riemann_integrable_on a,b
let a, b be Real; :: 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_divergent_to+infty_in b or Intf is_left_divergent_to-infty_in b ) ) implies not f is_right_ext_Riemann_integrable_on a,b )
assume 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_divergent_to+infty_in b or Intf is_left_divergent_to-infty_in b ) ) ; :: thesis: not f is_right_ext_Riemann_integrable_on a,b
then consider Intf being PartFunc of REAL,REAL such that
A1: dom Intf = [.a,b.[ and
A2: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) and
A3: ( Intf is_left_divergent_to+infty_in b or Intf is_left_divergent_to-infty_in b ) ;

hereby :: thesis: verum

assume f is_right_ext_Riemann_integrable_on a,b ; :: thesis: contradiction
then consider I being PartFunc of REAL,REAL such that
A4: dom I = [.a,b.[ and
A5: for x being Real st x in dom I holds
I . x = integral (f,a,x) and
A6: I is_left_convergent_in b by INTEGR10:def 1;

now :: thesis: for x being Element of REAL st x in dom I holds
I . x = Intf . x

let x be Element of REAL ; :: thesis: ( x in dom I implies I . x = Intf . x )
assume A7: x in dom I ; :: thesis: I . x = Intf . x
then I . x = integral (f,a,x) by A5;
hence I . x = Intf . x by A1, A4, A7, A2; :: thesis: verum

end;

then I = Intf by A1, A4, PARTFUN1:5;
hence contradiction by A3, A6, Th6, Th7; :: thesis: verum

end;