for R being Ring
for V being LeftMod of R
for L being Linear_Combination of V holds (0. R) * L = ZeroLC V by VECTSP_6:30;