for r being Real
for seq being Real_Sequence st seq is constant & ( r in rng seq or ex n being Nat st seq . n = r ) holds
lim seq = r