theorem Th12: :: COMSEQ_1:12

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