:: deftheorem Def2 defines SymGroup CAYLEY:def 2 :
for X being set
for b₂ being strict constituted-Functions multMagma holds
( b₂ = SymGroup X iff ( the carrier of b₂ = permutations X & ( for x, y being Element of b₂ holds x * y = y * x ) ) );