let r1, r2 be Real; :: thesis: ( ( for e being Real st e > 0 holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r1 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) ) & ( for e being Real st e > 0 holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r2 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) ) implies r1 = r2 )

assume that

A2: for e1 being Real st e1 > 0 holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r1 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e1 ) ) and

A3: for e2 being Real st e2 > 0 holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r2 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e2 ) ) ; :: thesis: r1 = r2

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r1 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) ) & ( for e being Real st e > 0 holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r2 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) ) implies r1 = r2 )

assume that

A2: for e1 being Real st e1 > 0 holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r1 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e1 ) ) and

A3: for e2 being Real st e2 > 0 holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r2 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e2 ) ) ; :: thesis: r1 = r2

A4: now :: thesis: for e3 being Real st e3 > 0 holds

|.(r1 - r2).| < e3

r1 = r2
|.(r1 - r2).| < e3

let e3 be Real; :: thesis: ( e3 > 0 implies |.(r1 - r2).| < e3 )

assume A5: e3 > 0 ; :: thesis: |.(r1 - r2).| < e3

set e4 = e3 / 2;

consider Y01 being finite Subset of X such that

not Y01 is empty and

A6: Y01 c= Y and

A7: for Y1 being finite Subset of X st Y01 c= Y1 & Y1 c= Y holds

|.(r1 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e3 / 2 by A2, A5, XREAL_1:139;

consider Y02 being finite Subset of X such that

not Y02 is empty and

A8: Y02 c= Y and

A9: for Y1 being finite Subset of X st Y02 c= Y1 & Y1 c= Y holds

|.(r2 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e3 / 2 by A3, A5, XREAL_1:139;

set Y00 = Y01 \/ Y02;

A10: ( (e3 / 2) + (e3 / 2) = e3 & Y01 c= Y01 \/ Y02 ) by XBOOLE_1:7;

A11: Y01 \/ Y02 c= Y by A6, A8, XBOOLE_1:8;

then |.(r2 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal))).| < e3 / 2 by A9, XBOOLE_1:7;

then ( |.((r1 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal))) - (r2 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal)))).| <= |.(r1 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal))).| + |.(r2 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal))).| & |.(r1 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal))).| + |.(r2 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal))).| < e3 ) by A7, A11, A10, COMPLEX1:57, XREAL_1:8;

hence |.(r1 - r2).| < e3 by XXREAL_0:2; :: thesis: verum

end;assume A5: e3 > 0 ; :: thesis: |.(r1 - r2).| < e3

set e4 = e3 / 2;

consider Y01 being finite Subset of X such that

not Y01 is empty and

A6: Y01 c= Y and

A7: for Y1 being finite Subset of X st Y01 c= Y1 & Y1 c= Y holds

|.(r1 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e3 / 2 by A2, A5, XREAL_1:139;

consider Y02 being finite Subset of X such that

not Y02 is empty and

A8: Y02 c= Y and

A9: for Y1 being finite Subset of X st Y02 c= Y1 & Y1 c= Y holds

|.(r2 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e3 / 2 by A3, A5, XREAL_1:139;

set Y00 = Y01 \/ Y02;

A10: ( (e3 / 2) + (e3 / 2) = e3 & Y01 c= Y01 \/ Y02 ) by XBOOLE_1:7;

A11: Y01 \/ Y02 c= Y by A6, A8, XBOOLE_1:8;

then |.(r2 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal))).| < e3 / 2 by A9, XBOOLE_1:7;

then ( |.((r1 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal))) - (r2 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal)))).| <= |.(r1 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal))).| + |.(r2 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal))).| & |.(r1 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal))).| + |.(r2 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal))).| < e3 ) by A7, A11, A10, COMPLEX1:57, XREAL_1:8;

hence |.(r1 - r2).| < e3 by XXREAL_0:2; :: thesis: verum

proof

hence
r1 = r2
; :: thesis: verum
assume A12:
r1 <> r2
; :: thesis: contradiction

A13: |.(r1 - r2).| <> 0

hence contradiction by A4, A13; :: thesis: verum

end;A13: |.(r1 - r2).| <> 0

proof

0 <= |.(r1 - r2).|
by COMPLEX1:46;
assume
|.(r1 - r2).| = 0
; :: thesis: contradiction

then r1 - r2 = 0 by ABSVALUE:2;

hence contradiction by A12; :: thesis: verum

end;then r1 - r2 = 0 by ABSVALUE:2;

hence contradiction by A12; :: thesis: verum

hence contradiction by A4, A13; :: thesis: verum