theorem Th27: :: INTEGR25:27

for f being PartFunc of REAL,REAL
for b being Real holds
( not f is_+infty_improper_integrable_on b or ( f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ) or ( not f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty (f,b) = +infty ) or ( not f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty (f,b) = -infty ) )