theorem Th14: :: TOPRNS_1:14

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