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