let f be PartFunc of REAL,REAL; :: thesis: for a being Real st f is_+infty_ext_Riemann_integrable_on a holds
f is_+infty_improper_integrable_on a
let a be Real; :: thesis: ( f is_+infty_ext_Riemann_integrable_on a implies f is_+infty_improper_integrable_on a )
assume A1: f is_+infty_ext_Riemann_integrable_on a ; :: thesis: f is_+infty_improper_integrable_on a
then 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 ) by INTEGR10:def 5;
hence f is_+infty_improper_integrable_on a by A1, INTEGR10:def 5; :: thesis: verum