for R being Ring
for V being LeftMod of R
for l being Linear_Combination of V holds l = l ! (Carrier l)