theorem Th32: :: VECTSP_2:32

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 * (0. R) = 0. V & v * (- (1_ R)) = - v & (0. V) * x = 0. V )