:: deftheorem Def6 defines improper_integral INTEGR24:def 6 :
for f being PartFunc of REAL,REAL
for a, b being Real st ].a,b.[ c= dom f & f is_improper_integrable_on a,b holds
for b₄ being ExtReal holds
( b₄ = improper_integral (f,a,b) iff ex c being Real st
( a < c & c < b & f is_left_improper_integrable_on a,c & f is_right_improper_integrable_on c,b & b₄ = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) ) );