let cF be complex-valued XFinSequence; :: thesis: cF is COMPLEX -valued
rng cF c= COMPLEX by VALUED_0:def 1;
hence cF is COMPLEX -valued by RELAT_1:def 19; :: thesis: verum