theorem Th3: :: CAYLEY:3

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