for A being non empty set
for x, y being Element of A
for f being Permutation of A holds
( f . x = y iff (f ") . y = x )