theorem :: PARTFUN1:47

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