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

proof

let x be set ; :: thesis: ( x in PFuncs X,{} iff x = {} )
thus ( x in PFuncs X,{} implies x = {} ) :: thesis: ( x = {} implies x in PFuncs X,{} )

proof

assume x in PFuncs X,{} ; :: thesis: x = {}
then x is PartFunc of X,{} by Th120;
hence x = {} ; :: thesis: verum

end;

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

end;

hence PFuncs X,{} = {{} } by TARSKI:def 1; :: thesis: verum