theorem Th18: :: VECTSP_1:22

for F being non empty right_complementable Abelian add-associative right_zeroed associative right_unital well-unital distributive doubleLoopStr
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F
for x being Element of F
for v being Element of V holds x * (- v) = - (x * v)