theorem :: CLVECT_1:11

for V being ComplexLinearSpace
for u, v being VECTOR of V
for z being Complex st z <> 0 & z * v = z * u holds
v = u