for x, y being Point of RNS st ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r ) & ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - y).|| < r ) holds
x = y

proof

given x, y being Point of RNS such that A2: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r and
A3: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - y).|| < r and
A4: x <> y ; :: thesis: contradiction
A5: ||.(x - y).|| <> 0 by A4, Th10;
then A6: 0 / 4 < ||.(x - y).|| / 4 by XREAL_1:74;
then consider m1 being Element of NAT such that
A7: for n being Element of NAT st m1 <= n holds
||.((S . n) - x).|| < ||.(x - y).|| / 4 by A2;
consider m2 being Element of NAT such that
A8: for n being Element of NAT st m2 <= n holds
||.((S . n) - y).|| < ||.(x - y).|| / 4 by A3, A6;

A9: now

||.(x - y).|| <= ||.(x - (S . m1)).|| + ||.((S . m1) - y).|| by Th14;
then A10: ||.(x - y).|| <= ||.((S . m1) - x).|| + ||.((S . m1) - y).|| by Th11;
assume m2 <= m1 ; :: thesis: contradiction
then A11: ||.((S . m1) - y).|| < ||.(x - y).|| / 4 by A8;
||.((S . m1) - x).|| < ||.(x - y).|| / 4 by A7;
then ||.((S . m1) - x).|| + ||.((S . m1) - y).|| < (||.(x - y).|| / 4) + (||.(x - y).|| / 4) by A11, XREAL_1:8;
then not ||.(x - y).|| / 2 < ||.(x - y).|| by A10, XXREAL_0:2;
hence contradiction by A5, XREAL_1:216; :: thesis: verum

end;

now

||.(x - y).|| <= ||.(x - (S . m2)).|| + ||.((S . m2) - y).|| by Th14;
then A12: ||.(x - y).|| <= ||.((S . m2) - x).|| + ||.((S . m2) - y).|| by Th11;
assume m1 <= m2 ; :: thesis: contradiction
then A13: ||.((S . m2) - x).|| < ||.(x - y).|| / 4 by A7;
||.((S . m2) - y).|| < ||.(x - y).|| / 4 by A8;
then ||.((S . m2) - x).|| + ||.((S . m2) - y).|| < (||.(x - y).|| / 4) + (||.(x - y).|| / 4) by A13, XREAL_1:8;
then not ||.(x - y).|| / 2 < ||.(x - y).|| by A12, XXREAL_0:2;
hence contradiction by A5, XREAL_1:216; :: thesis: verum

end;

hence contradiction by A9; :: thesis: verum

end;

hence for b₁, b₂ being Point of RNS st ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b₁).|| < r ) & ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b₂).|| < r ) holds
b₁ = b₂ ; :: thesis: verum