theorem :: PARTFUN1:10

for X, Y, Z being set
for f being PartFunc of X,Y holds f | Z is PartFunc of Z,Y