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