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 Lm4;
reconsider x9 = x1 as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider y9 = y1 as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:110;
A3: ( x + y = addcomplex .: x1,y1 & - y = compcomplex * y1 ) by SEQ_4:def 9, SEQ_4:def 11;
x + y = (len x) |-> 0c by A2, SEQ_4:def 15;
then x9 = - y9 by A1, A3, BINOP_2:1, FINSEQOP:78, SEQ_4:68, SEQ_4:69;
hence ( x = - y & y = - x ) ; :: thesis: verum