let f be NAT * -defined to-naturals homogeneous Function; :: thesis: f is Element of HFuncs NAT
A1: rng f c= NAT by VALUED_0:def 6;
dom f c= NAT * by RELAT_1:def 18;
then f is PartFunc of (NAT * ),NAT by A1, RELSET_1:11;
then reconsider f9 = f as Element of PFuncs (NAT * ),NAT by PARTFUN1:119;
f9 in { f1 where f1 is Element of PFuncs (NAT * ),NAT : f1 is homogeneous } ;
hence f is Element of HFuncs NAT ; :: thesis: verum