theorem Th1: :: MATRIXR2:1

for x, y being FinSequence of REAL st len x = len y & x + y = 0* (len x) holds
( x = - y & y = - x )