theorem Th34: :: VECTSP_2:34

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 being Vector of V holds (- v) * x = - (v * x)