let y1, y2 be ExtReal; :: 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) ) or ( Intf is_right_divergent_to+infty_in a & y1 = +infty ) or ( Intf is_right_divergent_to-infty_in a & y1 = -infty ) ) ) & 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) ) or ( Intf is_right_divergent_to+infty_in a & y2 = +infty ) or ( Intf is_right_divergent_to-infty_in a & y2 = -infty ) ) ) implies y1 = y2 )
assume that
A8: 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) ) or ( Intf is_right_divergent_to+infty_in a & y1 = +infty ) or ( Intf is_right_divergent_to-infty_in a & y1 = -infty ) ) ) and
A9: 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) ) or ( Intf is_right_divergent_to+infty_in a & y2 = +infty ) or ( Intf is_right_divergent_to-infty_in a & y2 = -infty ) ) ) ; :: thesis: y1 = y2
consider I0 being PartFunc of REAL,REAL such that
A10: ( dom I0 = ].a,b.] & ( for x being Real st x in dom I0 holds
I0 . x = integral (f,x,b) ) & ( I0 is_right_convergent_in a or I0 is_right_divergent_to+infty_in a or I0 is_right_divergent_to-infty_in a ) ) by A1;
consider I1 being PartFunc of REAL,REAL such that
A11: ( dom I1 = ].a,b.] & ( for x being Real st x in dom I1 holds
I1 . x = integral (f,x,b) ) & ( ( I1 is_right_convergent_in a & y1 = lim_right (I1,a) ) or ( I1 is_right_divergent_to+infty_in a & y1 = +infty ) or ( I1 is_right_divergent_to-infty_in a & y1 = -infty ) ) ) by A8;
consider I2 being PartFunc of REAL,REAL such that
A12: ( dom I2 = ].a,b.] & ( for x being Real st x in dom I2 holds
I2 . x = integral (f,x,b) ) & ( ( I2 is_right_convergent_in a & y2 = lim_right (I2,a) ) or ( I2 is_right_divergent_to+infty_in a & y2 = +infty ) or ( I2 is_right_divergent_to-infty_in a & y2 = -infty ) ) ) by A9;

now :: thesis: for x being Element of REAL st x in dom I0 holds
I0 . x = I1 . x

let x be Element of REAL ; :: thesis: ( x in dom I0 implies I0 . x = I1 . x )
assume A13: x in dom I0 ; :: thesis: I0 . x = I1 . x
then I0 . x = integral (f,x,b) by A10;
hence I0 . x = I1 . x by A11, A10, A13; :: thesis: verum

end;

then A14: I0 = I1 by A10, A11, PARTFUN1:5;

now :: thesis: for x being Element of REAL st x in dom I1 holds
I1 . x = I2 . x

let x be Element of REAL ; :: thesis: ( x in dom I1 implies I1 . x = I2 . x )
assume A15: x in dom I1 ; :: thesis: I1 . x = I2 . x
then I1 . x = integral (f,x,b) by A11;
hence I1 . x = I2 . x by A11, A12, A15; :: thesis: verum

end;

then A16: I1 = I2 by A11, A12, PARTFUN1:5;

per cases ( I0 is_right_convergent_in a or I0 is_right_divergent_to+infty_in a or I0 is_right_divergent_to-infty_in a ) by A10;

suppose I0 is_right_convergent_in a ; :: thesis: y1 = y2

thus y1 = y2 by A11, A12, A16, Th8, Th9; :: thesis: verum

end;

suppose I0 is_right_divergent_to+infty_in a ; :: thesis: y1 = y2

hence y1 = y2 by A11, A12, A16, A14, Th8; :: thesis: verum

end;

suppose I0 is_right_divergent_to-infty_in a ; :: thesis: y1 = y2

hence y1 = y2 by A11, A12, A16, A14, Th9; :: thesis: verum

end;

end;