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