theorem Th8: :: MATRIX_1:14

for n being Nat
for p being Element of Permutations n holds p " is Element of (Group_of_Perm n)