let L1, L2 be Real; :: 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 & L1 = lim_in-infty Intf ) & 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 & L2 = lim_in-infty Intf ) implies L1 = L2 )
assume ex Intf1 being PartFunc of REAL,REAL st
( dom Intf1 = left_closed_halfline b & ( for x being Real st x in dom Intf1 holds
Intf1 . x = integral (f,x,b) ) & Intf1 is convergent_in-infty & L1 = lim_in-infty Intf1 ) ; :: thesis: ( for Intf being PartFunc of REAL,REAL holds
( not dom Intf = left_closed_halfline b or ex x being Real st
( x in dom Intf & not Intf . x = integral (f,x,b) ) or not Intf is convergent_in-infty or not L2 = lim_in-infty Intf ) or L1 = L2 )
then consider Intf1 being PartFunc of REAL,REAL such that
A3: dom Intf1 = left_closed_halfline b and
A4: for x being Real st x in dom Intf1 holds
Intf1 . x = integral (f,x,b) and
Intf1 is convergent_in-infty and
A5: L1 = lim_in-infty Intf1 ;
assume ex Intf2 being PartFunc of REAL,REAL st
( dom Intf2 = left_closed_halfline b & ( for x being Real st x in dom Intf2 holds
Intf2 . x = integral (f,x,b) ) & Intf2 is convergent_in-infty & L2 = lim_in-infty Intf2 ) ; :: thesis: L1 = L2
then consider Intf2 being PartFunc of REAL,REAL such that
A6: dom Intf2 = left_closed_halfline b and
A7: for x being Real st x in dom Intf2 holds
Intf2 . x = integral (f,x,b) and
Intf2 is convergent_in-infty and
A8: L2 = lim_in-infty Intf2 ;

now :: thesis: for x being Element of REAL st x in dom Intf1 holds
Intf1 . x = Intf2 . x

let x be Element of REAL ; :: thesis: ( x in dom Intf1 implies Intf1 . x = Intf2 . x )
assume A9: x in dom Intf1 ; :: thesis: Intf1 . x = Intf2 . x
hence Intf1 . x = integral (f,x,b) by A4
.= Intf2 . x by A3, A6, A7, A9 ;
:: thesis: verum

end;

hence L1 = L2 by A3, A5, A6, A8, PARTFUN1:5; :: thesis: verum