theorem Th22: :: SEQ_1:22

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