( rng cf c= COMPLEX & rng (cf - X) c= rng cf ) by FINSEQ_3:66, VALUED_0:def 1;
then rng (cf - X) c= COMPLEX ;
hence cf - X is complex-valued by VALUED_0:def 1; :: thesis: verum