theorem :: COMSEQ_1:10

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