for X, Y being set
for f being Element of PFuncs (X,Y) holds f is PartFunc of X,Y by Th46;