theorem Th10: :: VECTSP_1:14

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