theorem Th19: :: INTEGR24:19

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