let a be real number ; :: thesis: for V being RealLinearSpace
for v being VECTOR of V holds
( not a * v = 0. V or a = 0 or v = 0. V )
let V be RealLinearSpace; :: thesis: for v being VECTOR of V holds
( not a * v = 0. V or a = 0 or v = 0. V )
let v be VECTOR of V; :: thesis: ( not a * v = 0. V or a = 0 or v = 0. V )
assume that
A1: a * v = 0. V and
A2: a <> 0 ; :: thesis: v = 0. V
thus v = 1 * v by Def9
.= ((a " ) * a) * v by A2, XCMPLX_0:def 7
.= (a " ) * (0. V) by A1, Def9
.= 0. V by Th23 ; :: thesis: verum