theorem Th16: :: COMSEQ_1:16

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