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