let f be PartFunc of REAL,REAL; :: thesis: for b being Real st ex Intf being PartFunc of REAL,REAL st
( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) & ( Intf is divergent_in-infty_to+infty or Intf is divergent_in-infty_to-infty ) ) holds
not f is_-infty_ext_Riemann_integrable_on b
let b be Real; :: thesis: ( ex Intf being PartFunc of REAL,REAL st
( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) & ( Intf is divergent_in-infty_to+infty or Intf is divergent_in-infty_to-infty ) ) implies not f is_-infty_ext_Riemann_integrable_on b )
assume ex Intf being PartFunc of REAL,REAL st
( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) & ( Intf is divergent_in-infty_to+infty or Intf is divergent_in-infty_to-infty ) ) ; :: thesis: not f is_-infty_ext_Riemann_integrable_on b
then consider Intf being PartFunc of REAL,REAL such that
A1: dom Intf = left_closed_halfline b and
A2: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
A3: ( Intf is divergent_in-infty_to+infty or Intf is divergent_in-infty_to-infty ) ;

hereby :: thesis: verum

assume f is_-infty_ext_Riemann_integrable_on b ; :: thesis: contradiction
then consider I being PartFunc of REAL,REAL such that
A4: dom I = left_closed_halfline b and
A5: for x being Real st x in dom I holds
I . x = integral (f,x,b) and
A6: I is convergent_in-infty by INTEGR10:def 6;

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

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

end;

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

end;