consider Intf being PartFunc of REAL ,REAL such that
A2: ( 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 A1, Def1;
take IT = lim_left Intf,b; :: thesis: 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 & IT = lim_left Intf,b )
thus 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 & IT = lim_left Intf,b ) by A2; :: thesis: verum