let V be ComplexLinearSpace; :: thesis: for v being VECTOR of V
for z being Complex st ( z = 0 or v = 0. V ) holds
z * v = 0. V
let v be VECTOR of V; :: thesis: for z being Complex st ( z = 0 or v = 0. V ) holds
z * v = 0. V
let z be Complex; :: thesis: ( ( z = 0 or v = 0. V ) implies z * v = 0. V )
assume A1: ( z = 0 or v = 0. V ) ; :: thesis: z * v = 0. V

now :: thesis: z * v = 0. V

per cases ( z = 0c or v = 0. V ) by A1;

suppose A2: z = 0c ; :: thesis: z * v = 0. V

v + (0c * v) = (1r * v) + (0c * v) by Def5
.= (1r + 0c) * v by Def3
.= v by Def5
.= v + (0. V) by RLVECT_1:4 ;
hence z * v = 0. V by A2, RLVECT_1:8; :: thesis: verum

end;

suppose A3: v = 0. V ; :: thesis: z * v = 0. V

(z * (0. V)) + (z * (0. V)) = z * ((0. V) + (0. V)) by Def2
.= z * (0. V) by RLVECT_1:4
.= (z * (0. V)) + (0. V) by RLVECT_1:4 ;
hence z * v = 0. V by A3, RLVECT_1:8; :: thesis: verum

end;

end;

end;

hence z * v = 0. V ; :: thesis: verum