theorem Th4: :: REAL_NS1:4

for n being Nat
for x being VECTOR of (REAL-NS n)
for a being Element of REAL n st x = a holds
- x = - a