for A being non empty set
for x being Element of A
for f being Permutation of A holds
( f . ((f ") . x) = x & (f ") . (f . x) = x ) by Th2;