for X being set
for f being Permutation of X holds
( (f ") * f = id X & f * (f ") = id X )