let x be complex-valued FinSequence; :: thesis: x + (- x) = 0c (len x)
A: ( x is FinSequence of COMPLEX & - x is FinSequence of COMPLEX ) by Lm4;
then reconsider x9 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:110;
x + (- x) = addcomplex .: x,(- x) by SEQ_4:def 9, A
.= addcomplex .: x,(compcomplex * x) by SEQ_4:def 11, A
.= (len x9) |-> 0c by BINOP_2:1, SEQ_4:68, SEQ_4:69, FINSEQOP:77
.= 0c (len x9) by SEQ_4:def 15 ;
hence x + (- x) = 0c (len x) ; :: thesis: verum