theorem Th81: :: MESFUN15:79

for f being PartFunc of REAL,REAL
for a, b being Real
for A being non empty Subset of REAL st ].a,b.] c= dom f & A = ].a,b.] & f is_left_improper_integrable_on a,b & abs f is_left_ext_Riemann_integrable_on a,b holds
( f | A is_integrable_on L-Meas & left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) )