theorem :: SEQ_1:6

for r being Real ex seq being Real_Sequence st rng seq = {r}