theorem Th2: :: COMSEQ_1:2

for f being Function holds
( f is Complex_Sequence iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of COMPLEX ) ) )