let f be to-naturals homogeneous from-natural-fseqs Function; :: thesis: f is Element of HFuncs NAT
( dom f c= NAT * & rng f c= NAT ) by Def2, 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