let Y be set ; :: thesis: PFuncs ({},Y) = {{}}
for x being object holds
( x in PFuncs ({},Y) iff x = {} )
proof
let x be object ; :: thesis: ( x in PFuncs ({},Y) iff x = {} )
thus ( x in PFuncs ({},Y) implies x = {} ) :: thesis: ( x = {} implies x in PFuncs ({},Y) )
proof
assume x in PFuncs ({},Y) ; :: thesis: x = {}
then x is PartFunc of {},Y by Th46;
hence x = {} ; :: thesis: verum
end;
{} is PartFunc of {},Y by RELSET_1:12;
hence ( x = {} implies x in PFuncs ({},Y) ) by Th45; :: thesis: verum
end;
hence PFuncs ({},Y) = {{}} by TARSKI:def 1; :: thesis: verum