theorem Th1: :: CLVECT_1:1

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