let f, Intf be PartFunc of REAL,REAL; :: thesis: 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)
let a, b be Real; :: thesis: ( 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 implies right_improper_integral (f,a,b) = lim_left (Intf,b) )
assume that
A1: f is_right_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,a,x) and
A4: Intf is_left_convergent_in b ; :: thesis: right_improper_integral (f,a,b) = lim_left (Intf,b)
A5: f is_right_ext_Riemann_integrable_on a,b by A1, A2, A3, A4, INTEGR10:def 1;
then A6: right_improper_integral (f,a,b) = ext_right_integral (f,a,b) by A1, Th39;
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,a,x) and
I is_left_convergent_in b and
A9: ext_right_integral (f,a,b) = lim_left (I,b) by A5, INTEGR10:def 3;

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,a,x) by A3;
hence Intf . x = I . x by A2, A7, A8, A10; :: thesis: verum

end;

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