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 A1;
take 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 & lim_in-infty Intf = 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 & lim_in-infty Intf = lim_in-infty Intf ) by A2; :: thesis: verum