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 A, SEQ_4:def 9
.= addcomplex .: x,(compcomplex * x) by A, SEQ_4:def 11
.= (len x9) |-> 0c by BINOP_2:1, FINSEQOP:77, SEQ_4:68, SEQ_4:69
.= 0c (len x9) by SEQ_4:def 15 ;
hence x + (- x) = 0c (len x) ; :: thesis: verum