theorem :: TOPRNS_1:8

for N being Nat
for r being Real
for seq being Real_Sequence of N holds |.(r * seq).| = |.r.| (#) |.seq.|