theorem Th8: :: VECTSP_1:12

for F being non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for x, y being Element of F holds
( x * y = 0. F iff ( x = 0. F or y = 0. F ) )