theorem Th1: :: MFOLD_2:1

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