theorem :: FUNCT_1:56

for Y being set
for f being Function holds dom (Y |` f) c= dom f by Th52;