let X be set ; :: thesis: {} in HFuncs X
set f = {} ;
( dom {} c= X * & rng {} c= X ) by XBOOLE_1:2;
then reconsider f = {} as PartFunc of (X * ),X by RELSET_1:11;
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