let X be ComplexNormSpace; :: thesis: for x, y being Point of X
for seq being Real_Sequence st seq is convergent & lim seq = 0 & ( for n being Element of 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 Element of NAT holds ||.(x - y).|| <= seq . n ) holds
x = y
let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = 0 & ( for n being Element of NAT holds ||.(x - y).|| <= seq . n ) implies x = y )
assume that
A1: ( seq is convergent & lim seq = 0 ) and
A2: for n being Element of NAT holds ||.(x - y).|| <= seq . n ; :: thesis: x = y

now

let e be Real; :: thesis: ( 0 < e implies ||.(x - y).|| < e )
assume 0 < e ; :: thesis: ||.(x - y).|| < e
then consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds
abs ((seq . m) - 0) < e by A1, SEQ_2:def 7;
A4: seq . n <= abs (seq . n) by ABSVALUE:4;
A5: ||.(x - y).|| <= seq . n by A2;
abs ((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