theorem Th3: :: COMSEQ_1:3

for seq being Complex_Sequence holds
( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0c )