let Y be set ; :: thesis: PFuncs ({},Y) = {{}}
for x being set holds
( x in PFuncs ({},Y) iff x = {} )

proof

let x be set ; :: 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 Th120;
hence x = {} ; :: thesis: verum

end;

{} is PartFunc of {},Y by RELSET_1:25;
hence ( x = {} implies x in PFuncs ({},Y) ) by Th119; :: thesis: verum

end;

hence PFuncs ({},Y) = {{}} by TARSKI:def 1; :: thesis: verum