theorem Th3: :: CLVECT_1:3
for V being ComplexLinearSpace
for v being VECTOR of V holds - v = (- 1r) * v