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