theorem Th6: :: CLVECT_1:6

for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex holds z * (- v) = (- z) * v