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:119;
f in { g where g is Element of PFuncs (X * ),X : g is homogeneous } ;
hence {} in HFuncs X ; :: thesis: verum