for f being PartFunc of REAL,REAL
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,x,b) ) & ( Intf is_right_divergent_to+infty_in a or Intf is_right_divergent_to-infty_in a ) ) holds
not f is_left_ext_Riemann_integrable_on a,b