for R being Ring
for V being LeftMod of R
for L being Linear_Combination of V
for a, b being Element of R holds a * (b * L) = (a * b) * L by VECTSP_6:34;