theorem Th20: :: INTEGR24:20

for f being PartFunc of REAL,REAL
for a, b, c being Real st a < b & b <= c & ].a,c.] c= dom f & f | ['b,c'] is bounded & f is_integrable_on ['b,c'] & f is_left_ext_Riemann_integrable_on a,b holds
( f is_left_ext_Riemann_integrable_on a,c & ext_left_integral (f,a,c) = (ext_left_integral (f,a,b)) + (integral (f,b,c)) )