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