for n being Nat ex P being non empty permutational set st len P = n