for x being Element of PFuncs X,Y holds x is PartFunc of X,Y by PARTFUN1:121;
hence PFuncs X,Y is PartFunc-set of X,Y by Def3; :: thesis: verum