theorem :: COMSEQ_1:31

for seq, seq1 being Complex_Sequence st seq is non-zero holds
(seq1 /" seq) (#) seq = seq1