let r be Real; :: thesis: ex seq being Real_Sequence st rng seq = {r}
consider f being Function such that
A1: dom f = NAT and
A2: rng f = {r} by FUNCT_1:5;
for x being object st x in {r} holds
x in REAL by XREAL_0:def 1;
then rng f c= REAL by A2, TARSKI:def 3;
then reconsider f = f as Real_Sequence by A1, FUNCT_2:def 1, RELSET_1:4;
take f ; :: thesis: rng f = {r}
thus rng f = {r} by A2; :: thesis: verum