A1: {x} c= INT by MEMBERED:5;
rng (X --> x) c= INT by A1, XBOOLE_1:1;
hence X --> x is integer-valued by Def5; :: thesis: verum