theorem :: PARTFUN1:39

for X, Y, Z being set
for f being Function holds Z |` <:f,X,Y:> = <:f,X,(Z /\ Y):>