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 * x) = v * (- x) & w - (v * x) = w + (v * (- x)) )