let y1, y2 be ExtReal; :: 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 & y1 = lim_in-infty Intf ) or ( Intf is divergent_in-infty_to+infty & y1 = +infty ) or ( Intf is divergent_in-infty_to-infty & y1 = -infty ) ) ) & 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 & y2 = lim_in-infty Intf ) or ( Intf is divergent_in-infty_to+infty & y2 = +infty ) or ( Intf is divergent_in-infty_to-infty & y2 = -infty ) ) ) implies y1 = y2 )
assume that
A8: 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 & y1 = lim_in-infty Intf ) or ( Intf is divergent_in-infty_to+infty & y1 = +infty ) or ( Intf is divergent_in-infty_to-infty & y1 = -infty ) ) ) and
A9: 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 & y2 = lim_in-infty Intf ) or ( Intf is divergent_in-infty_to+infty & y2 = +infty ) or ( Intf is divergent_in-infty_to-infty & y2 = -infty ) ) ) ; :: thesis: y1 = y2
consider I1 being PartFunc of REAL,REAL such that
A10: dom I1 = left_closed_halfline b and
A11: for x being Real st x in dom I1 holds
I1 . x = integral (f,x,b) and
A12: ( ( I1 is convergent_in-infty & y1 = lim_in-infty I1 ) or ( I1 is divergent_in-infty_to+infty & y1 = +infty ) or ( I1 is divergent_in-infty_to-infty & y1 = -infty ) ) by A8;
consider I2 being PartFunc of REAL,REAL such that
A13: dom I2 = left_closed_halfline b and
A14: for x being Real st x in dom I2 holds
I2 . x = integral (f,x,b) and
A15: ( ( I2 is convergent_in-infty & y2 = lim_in-infty I2 ) or ( I2 is divergent_in-infty_to+infty & y2 = +infty ) or ( I2 is divergent_in-infty_to-infty & y2 = -infty ) ) by A9;

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 A16: x in dom I1 ; :: thesis: I1 . x = I2 . x
then I1 . x = integral (f,x,b) by A11;
hence I1 . x = I2 . x by A10, A16, A13, A14; :: thesis: verum

end;

then I1 = I2 by A10, A13, PARTFUN1:5;
hence y1 = y2 by A12, A15, Th1, Th2; :: thesis: verum