reconsider n = n as Element of NAT by ORDINAL1:def 12;
dom f = NAT by PARTFUN1:def 2;
then A1: f . n in rng f by FUNCT_1:def 3;
rng f c= [:D,NAT:] by RELAT_1:def 19;
then (f . n) `2 in NAT by A1, MCART_1:10;
hence (f . n) `2 is natural ; :: thesis: verum