let f be PartFunc of REAL,REAL; :: thesis:
let a, b be Real; :: thesis:
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,x,b) ) & ( Intf is_right_divergent_to+infty_in a or Intf is_right_divergent_to-infty_in a ) ) ; :: thesis:
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,x,b) and
A3: ( Intf is_right_divergent_to+infty_in a or Intf is_right_divergent_to-infty_in a ) ;

hereby :: thesis:

assume f is_left_ext_Riemann_integrable_on a,b ; :: thesis:
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,x,b) and
A6: I is_right_convergent_in a by INTEGR10:def 2;

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

end;

then I = Intf by A1, A4, PARTFUN1:5;
hence contradiction by A3, A6, Th8, Th9; :: thesis:

end;