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