:: deftheorem Def7 defines infty_ext_right_integral INTEGR10:def 7 :
for f being PartFunc of REAL,REAL
for a being Real st f is_+infty_ext_Riemann_integrable_on a holds
for b₃ being Real holds
( b₃ = infty_ext_right_integral (f,a) iff ex Intf being PartFunc of REAL,REAL st
( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty & b₃ = lim_in+infty Intf ) );