set H = { f where f is Element of PFuncs (X * ),X : f is homogeneous } ;
( not { f where f is Element of PFuncs (X * ),X : f is homogeneous } is empty & { f where f is Element of PFuncs (X * ),X : f is homogeneous } is functional )

proof

{} is PartFunc of (X * ),X by RELSET_1:25;
then {} in PFuncs (X * ),X by PARTFUN1:119;
then {} in { f where f is Element of PFuncs (X * ),X : f is homogeneous } ;
hence not { f where f is Element of PFuncs (X * ),X : f is homogeneous } is empty ; :: thesis: { f where f is Element of PFuncs (X * ),X : f is homogeneous } is functional
let x be set ; :: according to FUNCT_1:def 19 :: thesis: ( not x in { f where f is Element of PFuncs (X * ),X : f is homogeneous } or x is set )
assume x in { f where f is Element of PFuncs (X * ),X : f is homogeneous } ; :: thesis: x is set
then ex g being Element of PFuncs (X * ),X st
( x = g & g is homogeneous ) ;
hence x is set ; :: thesis: verum

end;

then reconsider H = { f where f is Element of PFuncs (X * ),X : f is homogeneous } as non empty functional set ;

now

let f be Element of H; :: thesis: f is PartFunc of (X * ),X
f in H ;
then ex g being Element of PFuncs (X * ),X st
( f = g & g is homogeneous ) ;
hence f is PartFunc of (X * ),X ; :: thesis: verum

end;

hence { f where f is Element of PFuncs (X * ),X : f is homogeneous } is PFUNC_DOMAIN of X * ,X by RFUNCT_3:def 3; :: thesis: verum