for x, y being Point of RNS st ( for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r ) & ( for r being Real st 0 < r holds
ex m being Nat st
for n being 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 Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r and
A3: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - y).|| < r and
A4: x <> y ; :: thesis: contradiction
A5: ||.(x - y).|| <> 0 by A4, Th6;
then A6: 0 / 4 < ||.(x - y).|| / 4 ;
then consider m1 being Nat such that
A7: for n being Nat st m1 <= n holds
||.((S . n) - x).|| < ||.(x - y).|| / 4 by A2;
consider m2 being Nat such that
A8: for n being Nat st m2 <= n holds
||.((S . n) - y).|| < ||.(x - y).|| / 4 by A3, A6;
A9: now :: thesis: not m2 <= m1
||.(x - y).|| <= ||.(x - (S . m1)).|| + ||.((S . m1) - y).|| by Th10;
then A10: ||.(x - y).|| <= ||.((S . m1) - x).|| + ||.((S . m1) - y).|| by Th7;
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 :: thesis: not m1 <= m2
||.(x - y).|| <= ||.(x - (S . m2)).|| + ||.((S . m2) - y).|| by Th10;
then A12: ||.(x - y).|| <= ||.((S . m2) - x).|| + ||.((S . m2) - y).|| by Th7;
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 b1, b2 being Point of RNS st ( for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - b1).|| < r ) & ( for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - b2).|| < r ) holds
b1 = b2 ; :: thesis: verum