let x be FinSequence of COMPLEX ; :: thesis: x + (0c (len x)) = x
reconsider x9 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:110;
x + (0c (len x)) = x + ((len x) |-> 0c ) by COMPLSP1:def 13
.= addcomplex .: x,((len x) |-> 0c ) by COMPLSP1:def 7
.= x9 by BINOP_2:1, FINSEQOP:57 ;
hence x + (0c (len x)) = x ; :: thesis: verum