let y1, y2 be ExtReal; :: 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 & 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 = 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 & 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 = 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 & 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 = 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 & 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 = right_closed_halfline a and
A11: for x being Real st x in dom I1 holds
I1 . x = integral (f,a,x) 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 = right_closed_halfline a and
A14: for x being Real st x in dom I2 holds
I2 . x = integral (f,a,x) 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,a,x) 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, Th3, Th4; :: thesis: verum