for f being Function
for x being object st rng f = {x} holds
f = (dom f) --> x