theorem Th7: :: CLVECT_1:7

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