theorem :: COMSEQ_1:39

for seq being Complex_Sequence st seq is non-zero holds
- seq is non-zero by Th37;