:: deftheorem Def6 defines improper_integral_on_REAL INTEGR25:def 6 :
for f being PartFunc of REAL,REAL st dom f = REAL & f is_improper_integrable_on_REAL holds
for b₂ being ExtReal holds
( b₂ = improper_integral_on_REAL f iff ex c being Real st
( f is_-infty_improper_integrable_on c & f is_+infty_improper_integrable_on c & b₂ = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) ) );