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) ;

( 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 :: thesis: for x being Element of REAL st x in dom Intf1 holds

Intf1 . x = Intf2 . x

hence
y1 = y2
by A3, A5, A6, A8, PARTFUN1:5; :: thesis: verumIntf1 . 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;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