for S being non empty 1-sorted
for f being Function of S,S st f is idempotent holds
rng f = { x where x is Element of S : x = f . x }