for n being Nat holds idseq n is Element of (Group_of_Perm n)