theorem Th39: :: INTEGR24:39

for f being PartFunc of REAL,REAL
for a, b being Real holds
( not f is_right_improper_integrable_on a,b or ( f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = ext_right_integral (f,a,b) ) or ( not f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = +infty ) or ( not f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = -infty ) )