:: deftheorem DefR defines (*) RUSUB_6:def 1 :
for V being non empty RLSStruct
for r being FinSequence of REAL
for x, b₄ being FinSequence of V holds
( b₄ = r (*) x iff ( len b₄ = len x & ( for i being Nat st 1 <= i & i <= len x holds
b₄ . i = (r /. i) * (x /. i) ) ) );