theorem Th27: :: COMSEQ_1:27

for seq being Complex_Sequence st seq is non-zero holds
seq " is non-zero