for n being Nat holds permutations (Seg n) = Permutations n