theorem Th4: :: COMSEQ_1:4

for seq being Complex_Sequence holds
( seq is non-zero iff for n being Element of NAT holds seq . n <> 0c )