let y1, y2 be Real; :: thesis: ( ex Intf being PartFunc of REAL ,REAL st
( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds
Intf . x = integral f,x,b ) & Intf is_right_convergent_in a & y1 = lim_right Intf,a ) & ex Intf being PartFunc of REAL ,REAL st
( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds
Intf . x = integral f,x,b ) & Intf is_right_convergent_in a & y2 = lim_right Intf,a ) implies y1 = y2 )
assume ex Intf1 being PartFunc of REAL ,REAL st
( dom Intf1 = ].a,b.] & ( for x being Real st x in dom Intf1 holds
Intf1 . x = integral f,x,b ) & Intf1 is_right_convergent_in a & y1 = lim_right Intf1,a ) ; :: thesis: ( for Intf being PartFunc of REAL ,REAL holds
( not dom Intf = ].a,b.] or ex x being Real st
( x in dom Intf & not Intf . x = integral f,x,b ) or not Intf is_right_convergent_in a or not y2 = lim_right Intf,a ) or y1 = y2 )
then consider Intf1 being PartFunc of REAL ,REAL such that
A3: dom Intf1 = ].a,b.] and
A4: for x being Real st x in dom Intf1 holds
Intf1 . x = integral f,x,b and
Intf1 is_right_convergent_in a and
A5: y1 = lim_right Intf1,a ;
assume ex Intf2 being PartFunc of REAL ,REAL st
( dom Intf2 = ].a,b.] & ( for x being Real st x in dom Intf2 holds
Intf2 . x = integral f,x,b ) & Intf2 is_right_convergent_in a & y2 = lim_right Intf2,a ) ; :: thesis: y1 = y2
then consider Intf2 being PartFunc of REAL ,REAL such that
A6: dom Intf2 = ].a,b.] and
A7: for x being Real st x in dom Intf2 holds
Intf2 . x = integral f,x,b and
Intf2 is_right_convergent_in a and
A8: y2 = lim_right Intf2,a ;

now

let x be 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 y1 = y2 by A3, A5, A6, A8, PARTFUN1:34; :: thesis: verum