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