theorem Th28: :: COMSEQ_1:29

for seq, seq1 being Complex_Sequence holds
( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero )