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