rng F c= COMPLEX by VALUED_0:def 1;
then reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def 4;
take addcomplex $$ f ; :: thesis: ex f being FinSequence of COMPLEX st
( f = F & addcomplex $$ f = addcomplex $$ f )
thus ex f being FinSequence of COMPLEX st
( f = F & addcomplex $$ f = addcomplex $$ f ) ; :: thesis: verum