theorem Th15: :: SEQ_1:15

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