let X be set ; :: thesis: {} in HFuncs X
set f = {} ;
reconsider f = {} as PartFunc of (X *),X by XBOOLE_1:2;
reconsider f = f as Element of PFuncs ((X *),X) by PARTFUN1:45;
f in { g where g is Element of PFuncs ((X *),X) : g is homogeneous } ;
hence {} in HFuncs X ; :: thesis: verum