theorem Th11: :: PARTFUN1:11

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