let f, Intf be PartFunc of REAL,REAL; :: thesis: for a, b being Real st f is_left_improper_integrable_on a,b & dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a holds
left_improper_integral (f,a,b) = lim_right (Intf,a)
let a, b be Real; :: thesis: ( f is_left_improper_integrable_on a,b & dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a implies left_improper_integral (f,a,b) = lim_right (Intf,a) )
assume that
A1: f is_left_improper_integrable_on a,b and
A2: dom Intf = ].a,b.] and
A3: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
A4: Intf is_right_convergent_in a ; :: thesis: left_improper_integral (f,a,b) = lim_right (Intf,a)
A5: f is_left_ext_Riemann_integrable_on a,b by A1, A2, A3, A4, INTEGR10:def 2;
then A6: left_improper_integral (f,a,b) = ext_left_integral (f,a,b) by A1, Th34;
consider I being PartFunc of REAL,REAL such that
A7: dom I = ].a,b.] and
A8: for x being Real st x in dom I holds
I . x = integral (f,x,b) and
I is_right_convergent_in a and
A9: ext_left_integral (f,a,b) = lim_right (I,a) by A5, INTEGR10:def 4;

now :: thesis: for x being Element of REAL st x in dom Intf holds
Intf . x = I . x

let x be Element of REAL ; :: thesis: ( x in dom Intf implies Intf . x = I . x )
assume A10: x in dom Intf ; :: thesis: Intf . x = I . x
then Intf . x = integral (f,x,b) by A3;
hence Intf . x = I . x by A2, A7, A8, A10; :: thesis: verum

end;

hence left_improper_integral (f,a,b) = lim_right (Intf,a) by A6, A9, A2, A7, PARTFUN1:5; :: thesis: verum