theorem :: PARTFUN1:50

for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds
PFuncs (X1,Y1) c= PFuncs (X2,Y2)