for K being Ring
for r being Scalar of K
for V being LeftMod of K
for a being Vector of V
for v being Vector of ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) st a = v holds
r * a = r * v