theorem Th21: :: TOPRNS_1:21

for N being Nat
for r being Real
for seq being Real_Sequence of N st r <> 0 & seq is non-zero holds
r * seq is non-zero