:: deftheorem Def3 defines ext_right_integral INTEGR10:def 3 :
for f being PartFunc of REAL,REAL
for a, b being Real st f is_right_ext_Riemann_integrable_on a,b holds
for b₄ being Real holds
( b₄ = ext_right_integral (f,a,b) iff 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 & b₄ = lim_left (Intf,b) ) );