theorem :: INTEGR24:23

for f being PartFunc of REAL,REAL
for a, b being Real st ].a,b.] c= dom f & f is_left_ext_Riemann_integrable_on a,b holds
for c, d being Real st a <= c & c < d & d <= b holds
( f is_left_ext_Riemann_integrable_on c,d & ( a < c implies ext_left_integral (f,c,d) = integral (f,c,d) ) )