theorem :: COMSEQ_1:6

for r being Complex ex seq being Complex_Sequence st rng seq = {r}