let x, y be complex-valued FinSequence; ( 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)
; ( 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 )
; verum