theorem :: COMSEQ_1:19

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