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_1:14;
hence p " is Element of Permutations n by MATRIX_1:def 13; :: thesis: verum