theorem Th74: :: FUNCT_1:75

for Y being set
for f being Function holds f .: (f " Y) c= Y