let F be complex-valued FinSequence; :: thesis: F is FinSequence of COMPLEX
rng F c= COMPLEX by VALUED_0:def 1;
hence F is FinSequence of COMPLEX by FINSEQ_1:def 4; :: thesis: verum