k in NAT by ORDINAL1:def 13;
then ( rng (x --> k) c= {k} & {k} c= NAT ) by ZFMISC_1:37;
then rng (x --> k) c= NAT by XBOOLE_1:1;
hence x --> k is NAT -valued by RELAT_1:def 19; :: thesis: verum