theorem :: COMSEQ_1:35

for seq, seq1, seq2 being Complex_Sequence holds seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq