for R being Ring
for V being LeftMod of R
for v being VECTOR of V
for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) by VECTSP_6:40;