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