:: deftheorem defines * TOPRNS_1:def 3 :
for r being Real
for N being Nat
for seq being Real_Sequence of N holds r * seq = r (#) seq;