for x, y being Point of CNS 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 CNS 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: 0 <= ||.(x - y).|| by Th105;
A6: ||.(x - y).|| <> 0 by A4, Th107;
then consider m1 being Nat such that
A7: for n being Nat st m1 <= n holds
||.((S . n) - x).|| < ||.(x - y).|| / 4 by A2, A5;
consider m2 being Nat such that
A8: for n being Nat st m2 <= n holds
||.((S . n) - y).|| < ||.(x - y).|| / 4 by A3, A6, A5;
A9: now :: thesis: not m2 <= m1
||.(x - y).|| <= ||.(x - (S . m1)).|| + ||.((S . m1) - y).|| by Th111;
then A10: ||.(x - y).|| <= ||.((S . m1) - x).|| + ||.((S . m1) - y).|| by Th108;
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 A6, A5, XREAL_1:216; :: thesis: verum
end;
now :: thesis: not m1 <= m2
||.(x - y).|| <= ||.(x - (S . m2)).|| + ||.((S . m2) - y).|| by Th111;
then A12: ||.(x - y).|| <= ||.((S . m2) - x).|| + ||.((S . m2) - y).|| by Th108;
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 A6, A5, XREAL_1:216; :: thesis: verum
end;
hence contradiction by A9; :: thesis: verum
end;
hence for b1, b2 being Point of CNS 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