theorem :: PARTFUN1:13

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