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
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
; verum