let V be ComplexLinearSpace; :: thesis: for v being VECTOR of V
for z being Complex holds
( not z * v = 0. V or z = 0 or v = 0. V )
let v be VECTOR of V; :: thesis: for z being Complex holds
( not z * v = 0. V or z = 0 or v = 0. V )
let z be Complex; :: thesis: ( not z * v = 0. V or z = 0 or v = 0. V )
assume that
A1: z * v = 0. V and
A2: z <> 0 ; :: thesis: v = 0. V
thus v = 1r * v by Def5
.= ((z " ) * z) * v by A2, XCMPLX_0:def 7
.= (z " ) * (0. V) by A1, Def4
.= 0. V by Th2 ; :: thesis: verum