A1: {x} c= COMPLEX by MEMBERED:1;
rng (X --> x) c= COMPLEX by A1, XBOOLE_1:1;
hence X --> x is complex-valued by Def1; :: thesis: verum