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

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