set X = { g where g is NAT * -defined to-naturals homogeneous Function : f majorizes g } ;
{ g where g is NAT * -defined to-naturals homogeneous Function : f majorizes g } c= HFuncs NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { g where g is NAT * -defined to-naturals homogeneous Function : f majorizes g } or x in HFuncs NAT )
assume x in { g where g is NAT * -defined to-naturals homogeneous Function : f majorizes g } ; :: thesis: x in HFuncs NAT
then consider g being NAT * -defined to-naturals homogeneous Function such that
A1: x = g and
f majorizes g ;
g is Element of HFuncs NAT by COMPUT_1:28;
hence x in HFuncs NAT by A1; :: thesis: verum

end;

hence { g where g is NAT * -defined to-naturals homogeneous Function : f majorizes g } is Subset of (HFuncs NAT) ; :: thesis: verum