let x, y be FinSequence of REAL ; :: thesis: ( len x = len y & x + y = 0* (len x) implies ( x = - y & y = - x ) )
assume that
A1: len x = len y and
A2: x + y = 0* (len x) ; :: thesis: ( x = - y & y = - x )
A3: x = (0* (len x)) - y by A1, A2, MATRIXR1:14;
hence x = - y by A1, MATRIXR1:6; :: thesis: y = - x
thus - x = - (- y) by A1, A3, MATRIXR1:6
.= y ; :: thesis: verum