:: deftheorem Def5 defines * NORMSP_1:def 5 :
for RNS being non empty RLSStruct
for S being sequence of RNS
for a being Real
for b₄ being sequence of RNS holds
( b₄ = a * S iff for n being Nat holds b₄ . n = a * (S . n) );