theorem :: FUNCT_2:34

for X, Y, Z being set
for x being object
for f being Function of X,Y st Y <> {} & x in X & f . x in Z holds
(Z |` f) . x = f . x