for x, y being set
for f being Function holds Im ((f +* (x .--> y)),x) = {y}