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

proof

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

end;

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

end;

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