let r be Element of 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;

now

let x be set ; :: thesis: ( x in {r} implies x in COMPLEX )
assume x in {r} ; :: thesis: x in COMPLEX
then x = r by TARSKI:def 1;
hence x in COMPLEX ; :: thesis: verum

end;

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