let F be Field; :: thesis: for x being Element of F
for V being VectSp of F
for v being Element of V holds
( x * v = 0. V iff ( x = 0. F or v = 0. V ) )
let x be Element of F; :: thesis: for V being VectSp of F
for v being Element of V holds
( x * v = 0. V iff ( x = 0. F or v = 0. V ) )
let V be VectSp of F; :: thesis: for v being Element of V holds
( x * v = 0. V iff ( x = 0. F or v = 0. V ) )
let v be Element 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 A1: x * v = 0. V ; :: thesis: ( x = 0. F or v = 0. V )
assume A2: x <> 0. F ; :: thesis: v = 0. V
((x " ) * x) * v = (x " ) * (0. V) by A1, Def26
.= 0. V by Th59 ;
then 0. V = (1. F) * v by A2, Def22;
hence v = 0. V by Def26; :: thesis: verum

end;

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