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,x,b ) & Intf is_right_convergent_in a ) by A1, Def2;
take IT = lim_right Intf,a; :: 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,x,b ) & Intf is_right_convergent_in a & IT = lim_right Intf,a )
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,x,b ) & Intf is_right_convergent_in a & IT = lim_right Intf,a ) by A2; :: thesis: verum