let x be FinSequence of COMPLEX ; :: thesis: x + (- x) = 0c (len x)
reconsider x' = 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 x') |-> 0c by BINOP_2:1, COMPLSP1:7, COMPLSP1:8, FINSEQOP:77
.= 0c (len x') by COMPLSP1:def 13 ;
hence x + (- x) = 0c (len x) ; :: thesis: verum