let F be non degenerated almost_left_invertible Ring; :: thesis: 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 ) )
let x be Scalar of F; :: thesis: 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 ) )
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ModuleStr over F; :: thesis: for v being Vector of V holds
( x * v = 0. V iff ( x = 0. F or v = 0. V ) )
let v be Vector of V; :: thesis: ( x * v = 0. V iff ( x = 0. F or v = 0. V ) )
( not x * v = 0. V or x = 0. F or v = 0. V )

proof

assume x * v = 0. V ; :: thesis: ( x = 0. F or v = 0. V )
then A1: ((x ") * x) * v = (x ") * (0. V) by VECTSP_1:def 16
.= 0. V by VECTSP_1:14 ;
assume x <> 0. F ; :: thesis: v = 0. V
then 0. V = (1_ F) * v by A1, Th9;
hence v = 0. V by VECTSP_1:def 17; :: thesis: verum

end;

hence ( x * v = 0. V iff ( x = 0. F or v = 0. V ) ) by VECTSP_1:14; :: thesis: verum