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:12;
then {} in PFuncs ((X *),X) by PARTFUN1:45;
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 object ; :: according to FUNCT_1:def 13 :: 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 :: thesis: for f being Element of H holds f is PartFunc of (X *),X
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