A1: {x} c= NAT by MEMBERED:6;
rng (X --> x) c= NAT by A1, XBOOLE_1:1;
hence X --> x is natural-valued by Def6; :: thesis: verum