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