theorem Th13: :: TOPRNS_1:13

for N being Nat
for q, r being Real
for seq being Real_Sequence of N holds (r * q) * seq = r * (q * seq)