let x, y be complex-valued FinSequence; :: thesis: ( len x = len y & x + y = 0c (len x) implies ( x = - y & y = - x ) )
assume that
A1: len x = len y and
A2: x + y = 0c (len x) ; :: thesis: ( x = - y & y = - x )
reconsider x1 = x, y1 = y as FinSequence of COMPLEX by Lm2;
reconsider x9 = x1 as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9 = y1 as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:92;
A3: ( x + y = addcomplex .: (x1,y1) & - y = compcomplex * y1 ) by SEQ_4:def 6, SEQ_4:def 8;
x + y = (len x) |-> 0c by A2, SEQ_4:def 12;
then x9 = - y9 by A1, A3, BINOP_2:1, FINSEQOP:74, SEQ_4:51, SEQ_4:52;
hence ( x = - y & y = - x ) ; :: thesis: verum