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;
A6: 0 <= ||.(x - y).|| by Th8;
then A7: 0 / 4 < ||.(x - y).|| / 4 by A5, XREAL_1:76;
then consider m1 being Element of NAT such that
A8: 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
A9: for n being Element of NAT st m2 <= n holds
||.((S . n) - y).|| < ||.(x - y).|| / 4 by A3, A7;

A10: now

assume m1 <= m2 ; :: thesis: contradiction
then A11: ||.((S . m2) - x).|| < ||.(x - y).|| / 4 by A8;
||.((S . m2) - y).|| < ||.(x - y).|| / 4 by A9;
then A12: ||.((S . m2) - x).|| + ||.((S . m2) - y).|| < (||.(x - y).|| / 4) + (||.(x - y).|| / 4) by A11, XREAL_1:10;
||.(x - y).|| <= ||.(x - (S . m2)).|| + ||.((S . m2) - y).|| by Th14;
then ||.(x - y).|| <= ||.((S . m2) - x).|| + ||.((S . m2) - y).|| by Th11;
then not ||.(x - y).|| / 2 < ||.(x - y).|| by A12, XXREAL_0:2;
hence contradiction by A5, A6, XREAL_1:218; :: thesis: verum

end;

now

assume m2 <= m1 ; :: thesis: contradiction
then A13: ||.((S . m1) - y).|| < ||.(x - y).|| / 4 by A9;
||.((S . m1) - x).|| < ||.(x - y).|| / 4 by A8;
then A14: ||.((S . m1) - x).|| + ||.((S . m1) - y).|| < (||.(x - y).|| / 4) + (||.(x - y).|| / 4) by A13, XREAL_1:10;
||.(x - y).|| <= ||.(x - (S . m1)).|| + ||.((S . m1) - y).|| by Th14;
then ||.(x - y).|| <= ||.((S . m1) - x).|| + ||.((S . m1) - y).|| by Th11;
then not ||.(x - y).|| / 2 < ||.(x - y).|| by A14, XXREAL_0:2;
hence contradiction by A5, A6, XREAL_1:218; :: thesis: verum

end;

hence contradiction by A10; :: 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