consider Intf being PartFunc of REAL ,REAL such that
A2: ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds
Intf . x = integral f,a,x ) & Intf is convergent_in+infty ) by A1, Def5;
take IT = lim_in+infty Intf; :: thesis: ex Intf being PartFunc of REAL ,REAL st
( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds
Intf . x = integral f,a,x ) & Intf is convergent_in+infty & IT = lim_in+infty Intf )
thus ex Intf being PartFunc of REAL ,REAL st
( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds
Intf . x = integral f,a,x ) & Intf is convergent_in+infty & IT = lim_in+infty Intf ) by A2; :: thesis: verum