:: deftheorem Def3 defines SymGroupsIso CAYLEY:def 3 :
for X, Y being set
for p being Function of X,Y st X <> {} & Y <> {} & p is bijective holds
for b₄ being Function of (SymGroup X),(SymGroup Y) holds
( b₄ = SymGroupsIso p iff for x being Element of (SymGroup X) holds b₄ . x = (p * x) * (p ") );