let n, i 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 * by RELAT_1:def 18;
then n succ i is PartFunc of (NAT *),NAT by A1, RELSET_1:11;
then n succ i is Element of PFuncs ((NAT *),NAT) by PARTFUN1:119;
hence n succ i in HFuncs NAT ; :: thesis: verum