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