let x be FinSequence of COMPLEX ; :: thesis: x + (- x) = 0c (len x)
reconsider x9 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:110;
x + (- x) = addcomplex .: x,(- x) by COMPLSP1:def 7
.= addcomplex .: x,(compcomplex * x) by COMPLSP1:def 9
.= (len x9) |-> 0c by BINOP_2:1, COMPLSP1:7, COMPLSP1:8, FINSEQOP:77
.= 0c (len x9) by COMPLSP1:def 13 ;
hence x + (- x) = 0c (len x) ; :: thesis: verum