:: deftheorem defines is_equivalent_with GROUP_9:def 32 :
for O being set
for G1, G2 being GroupWithOperators of O
for s1 being CompositionSeries of G1
for s2 being CompositionSeries of G2 holds
( s1 is_equivalent_with s2 iff ( len s1 = len s2 & ( for n being Nat st n + 1 = len s1 holds
ex p being Permutation of (Seg n) st
for H1 being StableSubgroup of G1
for H2 being StableSubgroup of G2
for N1 being normal StableSubgroup of H1
for N2 being normal StableSubgroup of H2
for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds
H1 ./. N1,H2 ./. N2 are_isomorphic ) ) );