for X being RealNormSpace
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 )