let x be complex-valued FinSequence; :: thesis: x + (- x) = 0c (len x)
A1: ( x is FinSequence of COMPLEX & - x is FinSequence of COMPLEX ) by Lm2;
then reconsider x9 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
x + (- x) = addcomplex .: (x,(- x)) by A1, SEQ_4:def 6
.= addcomplex .: (x,(compcomplex * x)) by A1, SEQ_4:def 8
.= (len x9) |-> 0c by BINOP_2:1, FINSEQOP:73, SEQ_4:51, SEQ_4:52
.= 0c (len x9) by SEQ_4:def 12 ;
hence x + (- x) = 0c (len x) ; :: thesis: verum