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