for n being Nat
for perm being Element of Permutations n ex P being Permutation of (Permutations n) st
for p being Element of Permutations n holds P . p = p * perm