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