let X be RealNormSpace; :: thesis: for x, y being Point of X
for seq being Real_Sequence st seq is convergent & lim seq = 0 & ( for n being Nat holds ||.(x - y).|| <= seq . n ) holds
x = y
let x, y be Point of X; :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = 0 & ( for n being Nat holds ||.(x - y).|| <= seq . n ) holds
x = y
let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = 0 & ( for n being Nat holds ||.(x - y).|| <= seq . n ) implies x = y )
assume that
A1: ( seq is convergent & lim seq = 0 ) and
A2: for n being Nat holds ||.(x - y).|| <= seq . n ; :: thesis: x = y

now :: thesis: for e being Real st 0 < e holds
||.(x - y).|| < e

let e be Real; :: thesis: ( 0 < e implies ||.(x - y).|| < e )
assume 0 < e ; :: thesis: ||.(x - y).|| < e
then consider n being Nat such that
A3: for m being Nat st n <= m holds
|.((seq . m) - 0).| < e by A1, SEQ_2:def 7;
A4: seq . n <= |.(seq . n).| by ABSVALUE:4;
A5: ||.(x - y).|| <= seq . n by A2;
|.((seq . n) - 0).| < e by A3;
then seq . n < e by A4, XXREAL_0:2;
hence ||.(x - y).|| < e by A5, XXREAL_0:2; :: thesis: verum

end;

hence x = y by Lm2; :: thesis: verum