let n be Nat; :: thesis: for p being Element of Permutations n holds p " is Element of Permutations n
let p be Element of Permutations n; :: thesis: p " is Element of Permutations n
p " is Element of (Group_of_Perm n) by MATRIX_2:23;
hence p " is Element of Permutations n by MATRIX_2:def 10; :: thesis: verum