theorem Th17: :: COMSEQ_1:17

for r, p being Complex
for seq being Complex_Sequence holds (r * p) (#) seq = r (#) (p (#) seq)