theorem :: VECTSP_2:30

for F being non degenerated almost_left_invertible Ring
for x being Scalar of F
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ModuleStr over F
for v being Vector of V holds
( x * v = 0. V iff ( x = 0. F or v = 0. V ) )