:: deftheorem defines are_equivalent_under GROUP_9:def 34 :
for O being set
for f1, f2 being FinSequence
for p being Permutation of (dom f1) holds
( f1,f2 are_equivalent_under p,O iff ( len f1 = len f2 & ( for H1, H2 being GroupWithOperators of O
for i, j being Nat st i in dom f1 & j = (p ") . i & H1 = f1 . i & H2 = f2 . j holds
H1,H2 are_isomorphic ) ) );