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 Def12;
p " is Element of Permutations n by Def12;
hence p " is Element of (Group_of_Perm n) by Def13; :: thesis: verum