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,a,x) ) & ( ( Intf is_left_convergent_in b & y1 = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & y1 = +infty ) or ( Intf is_left_divergent_to-infty_in b & 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,a,x) ) & ( ( Intf is_left_convergent_in b & y2 = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & y2 = +infty ) or ( Intf is_left_divergent_to-infty_in b & 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,a,x) ) & ( ( Intf is_left_convergent_in b & y1 = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & y1 = +infty ) or ( Intf is_left_divergent_to-infty_in b & 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,a,x) ) & ( ( Intf is_left_convergent_in b & y2 = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & y2 = +infty ) or ( Intf is_left_divergent_to-infty_in b & 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,a,x) ) & ( I0 is_left_convergent_in b or I0 is_left_divergent_to+infty_in b or I0 is_left_divergent_to-infty_in b ) ) 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,a,x) ) & ( ( I1 is_left_convergent_in b & y1 = lim_left (I1,b) ) or ( I1 is_left_divergent_to+infty_in b & y1 = +infty ) or ( I1 is_left_divergent_to-infty_in b & 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,a,x) ) & ( ( I2 is_left_convergent_in b & y2 = lim_left (I2,b) ) or ( I2 is_left_divergent_to+infty_in b & y2 = +infty ) or ( I2 is_left_divergent_to-infty_in b & 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,a,x) 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,a,x) 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_left_convergent_in b or I0 is_left_divergent_to+infty_in b or I0 is_left_divergent_to-infty_in b ) by A10;
suppose I0 is_left_convergent_in b ; :: thesis: y1 = y2
thus y1 = y2 by A11, A12, A16, Th6, Th7; :: thesis: verum
end;
suppose I0 is_left_divergent_to+infty_in b ; :: thesis: y1 = y2
hence y1 = y2 by A11, A12, A14, A16, Th6; :: thesis: verum
end;
suppose I0 is_left_divergent_to-infty_in b ; :: thesis: y1 = y2
hence y1 = y2 by A11, A12, A14, A16, Th7; :: thesis: verum
end;
end;