let O be set ; :: thesis: for G1, G2 being GroupWithOperators of O
for s1 being CompositionSeries of G1
for s2 being CompositionSeries of G2 st s1 is empty & s2 is empty holds
s1 is_equivalent_with s2
let G1, G2 be GroupWithOperators of O; :: thesis: for s1 being CompositionSeries of G1
for s2 being CompositionSeries of G2 st s1 is empty & s2 is empty holds
s1 is_equivalent_with s2
let s1 be CompositionSeries of G1; :: thesis: for s2 being CompositionSeries of G2 st s1 is empty & s2 is empty holds
s1 is_equivalent_with s2
let s2 be CompositionSeries of G2; :: thesis: ( s1 is empty & s2 is empty implies s1 is_equivalent_with s2 )
assume A1: s1 is empty ; :: thesis: ( not s2 is empty or s1 is_equivalent_with s2 )
assume A2: s2 is empty ; :: thesis: s1 is_equivalent_with 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 by A1;
hence s1 is_equivalent_with s2 by A1, A2, Def35; :: thesis: verum