theorem Th4: :: CLVECT_1:4
for V being ComplexLinearSpace
for v being VECTOR of V st v = - v holds
v = 0. V