for f being PartFunc of REAL,REAL
for d being Real st left_closed_halfline d c= dom f & f is_-infty_ext_Riemann_integrable_on d holds
for b, c being Real st b < c & c <= d holds
( f is_right_ext_Riemann_integrable_on b,c & f is_left_ext_Riemann_integrable_on b,c )