let r be Complex; :: thesis: ex seq being Complex_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 COMPLEX by XCMPLX_0:def 2;

then rng f c= COMPLEX by A2, TARSKI:def 3;

then reconsider f = f as Complex_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 COMPLEX by XCMPLX_0:def 2;

then rng f c= COMPLEX by A2, TARSKI:def 3;

then reconsider f = f as Complex_Sequence by A1, FUNCT_2:def 1, RELSET_1:4;

take f ; :: thesis: rng f = {r}

thus rng f = {r} by A2; :: thesis: verum