:: deftheorem Def6 defines Group_of_Perm MATRIX_1:def 13 :
for n being Nat
for b₂ being strict multMagma holds
( b₂ = Group_of_Perm n iff ( the carrier of b₂ = Permutations n & ( for q, p being Element of Permutations n holds the multF of b₂ . (q,p) = p * q ) ) );