theorem :: FUNCT_4:8

for X, Y being set
for f being Function holds (Y |` f) | X c= f