let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st f is_right_ext_Riemann_integrable_on a,b holds
f is_right_improper_integrable_on a,b
let a, b be Real; :: thesis: ( f is_right_ext_Riemann_integrable_on a,b implies f is_right_improper_integrable_on a,b )
assume f is_right_ext_Riemann_integrable_on a,b ; :: thesis: f is_right_improper_integrable_on a,b
then ( ( for d being Real st a <= d & d < b holds
( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) ) & ex Intf being PartFunc of REAL,REAL st
( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b ) ) by INTEGR10:def 1;
hence f is_right_improper_integrable_on a,b ; :: thesis: verum