theorem :: MESFUN15:40

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_right_improper_integrable_on a,b & f | A is nonpositive holds
( right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( f is_right_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_right_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = -infty ) )