let n be Nat; :: thesis: idseq n is Element of (Group_of_Perm n)
the carrier of (Group_of_Perm n) = Permutations n by Def10;
hence idseq n is Element of (Group_of_Perm n) by Def9; :: thesis: verum