let X be RealNormSpace; :: thesis: for x being Point of X
for seq being sequence of X st ( for n being Nat holds seq . n = x ) holds
( seq is convergent & lim seq = x )
let x be Point of X; :: thesis: for seq being sequence of X st ( for n being Nat holds seq . n = x ) holds
( seq is convergent & lim seq = x )
let seq be sequence of X; :: thesis: ( ( for n being Nat holds seq . n = x ) implies ( seq is convergent & lim seq = x ) )
assume A1: for n being Nat holds seq . n = x ; :: thesis: ( seq is convergent & lim seq = x )

now :: thesis: for z, w being object st z in dom seq & w in dom seq holds
seq . z = seq . w

let z, w be object ; :: thesis: ( z in dom seq & w in dom seq implies seq . z = seq . w )
assume ( z in dom seq & w in dom seq ) ; :: thesis: seq . z = seq . w
then reconsider n1 = z, n2 = w as Nat ;
thus seq . z = seq . n1
.= x by A1
.= seq . n2 by A1
.= seq . w ; :: thesis: verum

end;

then A2: seq is constant by FUNCT_1:def 10;
hence seq is convergent by NDIFF_1:18; :: thesis: lim seq = x
thus lim seq = seq . 0 by A2, NDIFF_1:18
.= x by A1 ; :: thesis: verum