for X being RealUnitarySpace
for x being Point of X
for seq being sequence of X st seq is constant & ex n being Nat st seq . n = x holds
lim seq = x