theorem :: VECTSP_2:35

for R being non empty right_complementable right_unital well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for V being non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over R
for x being Scalar of R
for v, w being Vector of V holds (v - w) * x = (v * x) - (w * x)