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
A6: ||.(x - y).|| <> 0 by A4, Th10;
then A7: 0 / 4 < ||.(x - y).|| / 4 by 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

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

end;

now

||.(x - y).|| <= ||.(x - (S . m2)).|| + ||.((S . m2) - y).|| by Th14;
then A13: ||.(x - y).|| <= ||.((S . m2) - x).|| + ||.((S . m2) - y).|| by Th11;
assume m1 <= m2 ; :: thesis: contradiction
then A14: ||.((S . m2) - x).|| < ||.(x - y).|| / 4 by A8;
||.((S . m2) - y).|| < ||.(x - y).|| / 4 by A9;
then ||.((S . m2) - x).|| + ||.((S . m2) - y).|| < (||.(x - y).|| / 4) + (||.(x - y).|| / 4) by A14, XREAL_1:10;
then not ||.(x - y).|| / 2 < ||.(x - y).|| by A13, XXREAL_0:2;
hence contradiction by 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