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