for X being RealUnitarySpace
for seq being sequence of X st seq is constant holds
seq is convergent ;