theorem Th2: :: CLVECT_1:2

for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex holds
( not z * v = 0. V or z = 0 or v = 0. V )