for X being set
for f being Function of X,X st f is one-to-one & rng f = X holds
f is Permutation of X