:: deftheorem Def6 defines (#) RMOD_4:def 6 :
for R being Ring
for V being RightMod of R
for F being FinSequence of V
for f being Function of V,R
for b₅ being FinSequence of V holds
( b₅ = f (#) F iff ( len b₅ = len F & ( for i being Nat st i in dom b₅ holds
b₅ . i = (F /. i) * (f . (F /. i)) ) ) );