let r1, r2 be Real; ( ( 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 ) )
; r1 = r2
A4:
now for e3 being Real st e3 > 0 holds
|.(r1 - r2).| < e3let e3 be
Real;
( e3 > 0 implies |.(r1 - r2).| < e3 )assume A5:
e3 > 0
;
|.(r1 - r2).| < e3set 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;
verum end;
r1 = r2
hence
r1 = r2
; verum