theorem :: FUNCT_1:78

for Y being set
for f being Function holds f .: (f " Y) = Y /\ (f .: (dom f))