theorem Th1: :: COMSEQ_1:1

for f being Function holds
( f is Complex_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of COMPLEX ) ) )