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

rng F c= COMPLEX by VALUED_0:def 1;

hence F is FinSequence of COMPLEX by FINSEQ_1:def 4; :: thesis: verum