let y1, y2 be Point of X; :: 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

||.(y1 - (setsum Y1)).|| < 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

||.(y2 - (setsum Y1)).|| < e ) ) ) implies y1 = y2 )

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

||.(y1 - (setsum Y1)).|| < 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

||.(y2 - (setsum Y1)).|| < e2 ) ) ; :: thesis: y1 = y2

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

||.(y1 - (setsum Y1)).|| < 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

||.(y2 - (setsum Y1)).|| < e ) ) ) implies y1 = y2 )

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

||.(y1 - (setsum Y1)).|| < 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

||.(y2 - (setsum Y1)).|| < e2 ) ) ; :: thesis: y1 = y2

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

||.(y1 - y2).|| < e3

y1 = y2
||.(y1 - y2).|| < e3

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

assume A5: e3 > 0 ; :: thesis: ||.(y1 - y2).|| < 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

||.(y1 - (setsum Y1)).|| < 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

||.(y2 - (setsum Y1)).|| < 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 ||.(y2 - (setsum (Y01 \/ Y02))).|| < e3 / 2 by A9, XBOOLE_1:7;

then ||.(- (y2 - (setsum (Y01 \/ Y02)))).|| < e3 / 2 by BHSP_1:31;

then ||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).|| < e3 by A7, A11, A10, XREAL_1:8;

then ||.((y1 - (setsum (Y01 \/ Y02))) + (- (y2 - (setsum (Y01 \/ Y02))))).|| + (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||) < (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||) + e3 by BHSP_1:30, XREAL_1:8;

then A12: (||.((y1 - (setsum (Y01 \/ Y02))) + (- (y2 - (setsum (Y01 \/ Y02))))).|| + (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||)) + (- (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||)) < (e3 + (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||)) + (- (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||)) by XREAL_1:8;

||.(y1 - y2).|| = ||.((y1 - y2) + (0. X)).|| by RLVECT_1:def 4

.= ||.((y1 - y2) + ((setsum (Y01 \/ Y02)) - (setsum (Y01 \/ Y02)))).|| by RLVECT_1:5

.= ||.(((y1 - y2) + (setsum (Y01 \/ Y02))) - (setsum (Y01 \/ Y02))).|| by RLVECT_1:def 3

.= ||.((y1 - (y2 - (setsum (Y01 \/ Y02)))) - (setsum (Y01 \/ Y02))).|| by RLVECT_1:29

.= ||.(y1 - ((setsum (Y01 \/ Y02)) + (y2 - (setsum (Y01 \/ Y02))))).|| by RLVECT_1:27

.= ||.((y1 - (setsum (Y01 \/ Y02))) - (y2 - (setsum (Y01 \/ Y02)))).|| by RLVECT_1:27

.= ||.((y1 - (setsum (Y01 \/ Y02))) + (- (y2 - (setsum (Y01 \/ Y02))))).|| ;

hence ||.(y1 - y2).|| < e3 by A12; :: thesis: verum

end;assume A5: e3 > 0 ; :: thesis: ||.(y1 - y2).|| < 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

||.(y1 - (setsum Y1)).|| < 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

||.(y2 - (setsum Y1)).|| < 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 ||.(y2 - (setsum (Y01 \/ Y02))).|| < e3 / 2 by A9, XBOOLE_1:7;

then ||.(- (y2 - (setsum (Y01 \/ Y02)))).|| < e3 / 2 by BHSP_1:31;

then ||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).|| < e3 by A7, A11, A10, XREAL_1:8;

then ||.((y1 - (setsum (Y01 \/ Y02))) + (- (y2 - (setsum (Y01 \/ Y02))))).|| + (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||) < (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||) + e3 by BHSP_1:30, XREAL_1:8;

then A12: (||.((y1 - (setsum (Y01 \/ Y02))) + (- (y2 - (setsum (Y01 \/ Y02))))).|| + (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||)) + (- (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||)) < (e3 + (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||)) + (- (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||)) by XREAL_1:8;

||.(y1 - y2).|| = ||.((y1 - y2) + (0. X)).|| by RLVECT_1:def 4

.= ||.((y1 - y2) + ((setsum (Y01 \/ Y02)) - (setsum (Y01 \/ Y02)))).|| by RLVECT_1:5

.= ||.(((y1 - y2) + (setsum (Y01 \/ Y02))) - (setsum (Y01 \/ Y02))).|| by RLVECT_1:def 3

.= ||.((y1 - (y2 - (setsum (Y01 \/ Y02)))) - (setsum (Y01 \/ Y02))).|| by RLVECT_1:29

.= ||.(y1 - ((setsum (Y01 \/ Y02)) + (y2 - (setsum (Y01 \/ Y02))))).|| by RLVECT_1:27

.= ||.((y1 - (setsum (Y01 \/ Y02))) - (y2 - (setsum (Y01 \/ Y02)))).|| by RLVECT_1:27

.= ||.((y1 - (setsum (Y01 \/ Y02))) + (- (y2 - (setsum (Y01 \/ Y02))))).|| ;

hence ||.(y1 - y2).|| < e3 by A12; :: thesis: verum

proof

hence
y1 = y2
; :: thesis: verum
assume
y1 <> y2
; :: thesis: contradiction

then y1 - y2 <> 0. X by VECTSP_1:19;

then A13: ||.(y1 - y2).|| <> 0 by BHSP_1:26;

0 <= ||.(y1 - y2).|| by BHSP_1:28;

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

end;then y1 - y2 <> 0. X by VECTSP_1:19;

then A13: ||.(y1 - y2).|| <> 0 by BHSP_1:26;

0 <= ||.(y1 - y2).|| by BHSP_1:28;

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