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