theorem :: INTEGR24:41

for f, Intf being PartFunc of REAL,REAL
for a, b being Real st f is_right_improper_integrable_on a,b & 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 holds
right_improper_integral (f,a,b) = lim_left (Intf,b)