A1: {x} c= REAL by MEMBERED:3;
rng (X --> x) c= REAL by A1, XBOOLE_1:1;
hence X --> x is real-valued by Def3; :: thesis: verum