theorem Th22: :: INTEGR24:22

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 d being Real st a < d & d <= b holds
( f is_left_ext_Riemann_integrable_on a,d & ext_left_integral (f,a,b) = (ext_left_integral (f,a,d)) + (integral (f,d,b)) )