:: deftheorem defines <: LMOD_6:def 4 :
for K being Ring
for V being LeftMod of K
for a being Vector of V holds <:a:> = Lin {a};