for n being Nat holds idseq n = 1_ (Group_of_Perm n)