let x be complex-valued FinSequence; :: thesis: x + (0c (len x)) = x
A1: x is FinSequence of COMPLEX by Lm2;
then reconsider x9 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
x + (0c (len x)) = x + ((len x) |-> 0c) by SEQ_4:def 12
.= addcomplex .: (x,((len x) |-> 0c)) by A1, SEQ_4:def 6
.= x9 by BINOP_2:1, FINSEQOP:56 ;
hence x + (0c (len x)) = x ; :: thesis: verum