theorem :: CAYLEY:8

for n being Nat holds SymGroup (Seg n) = Group_of_Perm n