theorem Th2: :: MFOLD_2:2

for f being Function
for Y1, Y2 being set st Y2 c= Y1 holds
(Y1 |` f) " Y2 = f " Y2