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

now

let x be Real; :: thesis: ( x in dom Intf1 implies Intf1 . x = Intf2 . x )
assume A7: x in dom Intf1 ; :: thesis: Intf1 . x = Intf2 . x
thus Intf1 . x = integral f,a,x by A5, A7
.= Intf2 . x by A5, A6, A7 ; :: thesis: verum

end;

hence L1 = L2 by A5, A6, PARTFUN1:34; :: thesis: verum