for V being ComplexLinearSpace
for v being VECTOR of V
for z1, z2 being Complex st v <> 0. V & z1 * v = z2 * v holds
z1 = z2