:: deftheorem Def10 defines * RMOD_4:def 10 :
for R being Ring
for V being RightMod of R
for a being Scalar of R
for L, b₅ being Linear_Combination of V holds
( b₅ = L * a iff for v being Vector of V holds b₅ . v = (L . v) * a );