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

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