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