theorem Th9: :: COMSEQ_1:9

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