for S being non empty 1-sorted
for f being Function of S,S st f is idempotent holds
for x being Element of S holds f . (f . x) = f . x