theorem Th45: :: MESFUN15:43

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_improper_integrable_on a,b & f | A is nonnegative holds
( improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( ex c being Real st
( a < c & c < b & f is_left_ext_Riemann_integrable_on a,c & f is_right_ext_Riemann_integrable_on c,b ) implies f | A is_integrable_on L-Meas ) & ( ( for c being Real st a < c & c < b & f is_left_ext_Riemann_integrable_on a,c holds
not f is_right_ext_Riemann_integrable_on c,b ) implies Integral (L-Meas,(f | A)) = +infty ) )