let f be PartFunc of REAL,REAL; :: thesis: for b being Real st f is_-infty_ext_Riemann_integrable_on b holds
f is_-infty_improper_integrable_on b
let b be Real; :: thesis: ( f is_-infty_ext_Riemann_integrable_on b implies f is_-infty_improper_integrable_on b )
assume A1: f is_-infty_ext_Riemann_integrable_on b ; :: thesis: f is_-infty_improper_integrable_on b
then ex Intf being PartFunc of REAL,REAL st
( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) & Intf is convergent_in-infty ) by INTEGR10:def 6;
hence f is_-infty_improper_integrable_on b by A1, INTEGR10:def 6; :: thesis: verum