let i, n be Nat; :: thesis: n proj i in HFuncs NAT
set X = NAT ;
set f = n proj i;
A1: rng (n proj i) c= NAT by VALUED_0:def 6;
dom (n proj i) c= NAT * ;
then n proj i is PartFunc of (NAT *),NAT by A1, RELSET_1:4;
then n proj i is Element of PFuncs ((NAT *),NAT) by PARTFUN1:45;
hence n proj i in HFuncs NAT ; :: thesis: verum