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