theorem Th13: :: COMSEQ_1:13

for r being Complex
for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)