let n, m be Element of 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 * by RELAT_1:def 18;
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