theorem Th12: :: TOPRNS_1:12

for N being Nat
for r being Real
for seq1, seq2 being Real_Sequence of N holds r * (seq1 + seq2) = (r * seq1) + (r * seq2)