let n be Nat; :: thesis: for p being Element of Permutations n holds p " is Element of (Group_of_Perm n)

let p be Element of Permutations n; :: thesis: p " is Element of (Group_of_Perm n)

reconsider p = p as Permutation of (Seg n) by Def5;

p " is Element of Permutations n by Def5;

hence p " is Element of (Group_of_Perm n) by Def6; :: thesis: verum

let p be Element of Permutations n; :: thesis: p " is Element of (Group_of_Perm n)

reconsider p = p as Permutation of (Seg n) by Def5;

p " is Element of Permutations n by Def5;

hence p " is Element of (Group_of_Perm n) by Def6; :: thesis: verum