theorem :: FUNCT_1:113

for Y being set
for f being Function holds Y |` f = f | (f " Y)