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 not s1 is empty & not s2 is empty holds
( s1 is_equivalent_with s2 iff ex p being Permutation of () st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

let G1, G2 be GroupWithOperators of O; :: thesis: for s1 being CompositionSeries of G1
for s2 being CompositionSeries of G2 st not s1 is empty & not s2 is empty holds
( s1 is_equivalent_with s2 iff ex p being Permutation of () st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

let s1 be CompositionSeries of G1; :: thesis: for s2 being CompositionSeries of G2 st not s1 is empty & not s2 is empty holds
( s1 is_equivalent_with s2 iff ex p being Permutation of () st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

let s2 be CompositionSeries of G2; :: thesis: ( not s1 is empty & not s2 is empty implies ( s1 is_equivalent_with s2 iff ex p being Permutation of () st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O ) )
assume that
A1: not s1 is empty and
A2: not s2 is empty ; :: thesis: ( s1 is_equivalent_with s2 iff ex p being Permutation of () st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )
set f2 = the_series_of_quotients_of s2;
set f1 = the_series_of_quotients_of s1;
hereby :: thesis: ( ex p being Permutation of () st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O implies s1 is_equivalent_with s2 )
assume A3: s1 is_equivalent_with s2 ; :: thesis: ex p being Permutation of () st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O
then A4: len s1 = len s2 ;
per cases ( len s1 <= 1 or len s1 > 1 ) ;
suppose A5: len s1 <= 1 ; :: thesis: ex p being Permutation of () st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O
reconsider fs1 = the_series_of_quotients_of s1, fs2 = the_series_of_quotients_of s2 as FinSequence ;
set p = the Permutation of ();
reconsider pf = the Permutation of () as Permutation of (dom fs1) ;
fs1 = {} by ;
then A6: for H1, H2 being GroupWithOperators of O
for i, j being Nat st i in dom fs1 & j = (pf ") . i & H1 = fs1 . i & H2 = fs2 . j holds
H1,H2 are_isomorphic ;
take p = the Permutation of (); :: thesis:
fs2 = {} by ;
then len = len by ;
hence the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O by A6; :: thesis: verum
end;
suppose A7: len s1 > 1 ; :: thesis: ex p9 being Permutation of () st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p9,O
set n = (len s1) - 1;
(len s1) - 1 > 1 - 1 by ;
then (len s1) - 1 in NAT by INT_1:3;
then reconsider n = (len s1) - 1 as Nat ;
n + 1 = len s1 ;
then consider p being Permutation of (Seg n) such that
A8: 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 A3;
A9: len s1 = () + 1 by ;
then dom = Seg n by FINSEQ_1:def 3;
then reconsider p9 = p " as Permutation of () ;
reconsider fs1 = the_series_of_quotients_of s1, fs2 = the_series_of_quotients_of s2 as FinSequence ;
A10: len s2 = () + 1 by ;
reconsider pf = p9 as Permutation of (dom fs1) ;
take p9 = p9; :: thesis:
A11: pf " = p by FUNCT_1:43;
now :: thesis: for H19, H29 being GroupWithOperators of O
for i, j being Nat st i in dom fs1 & j = (pf ") . i & H19 = fs1 . i & H29 = fs2 . j holds
H19,H29 are_isomorphic
let H19, H29 be GroupWithOperators of O; :: thesis: for i, j being Nat st i in dom fs1 & j = (pf ") . i & H19 = fs1 . i & H29 = fs2 . j holds
H19,H29 are_isomorphic

let i, j be Nat; :: thesis: ( i in dom fs1 & j = (pf ") . i & H19 = fs1 . i & H29 = fs2 . j implies H19,H29 are_isomorphic )
set H1 = s1 . i;
set H2 = s2 . j;
set N1 = s1 . (i + 1);
set N2 = s2 . (j + 1);
assume A12: i in dom fs1 ; :: thesis: ( j = (pf ") . i & H19 = fs1 . i & H29 = fs2 . j implies H19,H29 are_isomorphic )
then A13: i in Seg (len fs1) by FINSEQ_1:def 3;
then A14: 1 <= i by FINSEQ_1:1;
A15: i <= len fs1 by ;
then A16: i + 1 <= (len fs1) + 1 by XREAL_1:6;
0 + i < 1 + i by XREAL_1:6;
then 1 <= i + 1 by ;
then i + 1 in Seg (len s1) by ;
then A17: i + 1 in dom s1 by FINSEQ_1:def 3;
assume A18: j = (pf ") . i ; :: thesis: ( H19 = fs1 . i & H29 = fs2 . j implies H19,H29 are_isomorphic )
0 + (len fs1) < 1 + (len fs1) by XREAL_1:6;
then i <= len s1 by ;
then i in Seg (len s1) by A14;
then A19: i in dom s1 by FINSEQ_1:def 3;
then reconsider H1 = s1 . i, N1 = s1 . (i + 1) as Element of the_stable_subgroups_of G1 by ;
reconsider H1 = H1, N1 = N1 as StableSubgroup of G1 by Def11;
reconsider N1 = N1 as normal StableSubgroup of H1 by ;
assume that
A20: H19 = fs1 . i and
A21: H29 = fs2 . j ; :: thesis: H19,H29 are_isomorphic
i in dom p by ;
then A22: j in rng p by ;
then A23: 1 <= j by FINSEQ_1:1;
A24: j <= len fs2 by ;
then A25: j + 1 <= (len fs2) + 1 by XREAL_1:6;
0 + j < 1 + j by XREAL_1:6;
then 1 <= j + 1 by ;
then j + 1 in Seg (len s2) by ;
then A26: j + 1 in dom s2 by FINSEQ_1:def 3;
0 + (len fs2) < 1 + (len fs2) by XREAL_1:6;
then j <= len s2 by ;
then j in Seg (len s2) by A23;
then A27: j in dom s2 by FINSEQ_1:def 3;
then reconsider H2 = s2 . j, N2 = s2 . (j + 1) as Element of the_stable_subgroups_of G2 by ;
reconsider H2 = H2, N2 = N2 as StableSubgroup of G2 by Def11;
reconsider N2 = N2 as normal StableSubgroup of H2 by ;
dom fs1 = Seg n by ;
then ( 1 <= i & i <= n ) by ;
then A28: H1 ./. N1,H2 ./. N2 are_isomorphic by A8, A11, A18;
j in Seg () by A4, A10, A22;
then j in dom fs2 by FINSEQ_1:def 3;
then H2 ./. N2 = H29 by A4, A7, A21, Def33;
hence H19,H29 are_isomorphic by A7, A12, A20, A28, Def33; :: thesis: verum
end;
hence the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p9,O by A4, A9, A10; :: thesis: verum
end;
end;
end;
given p being Permutation of () such that A29: the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O ; :: thesis:
A30: len = len by A29;
per cases ( len s1 <= 1 or len s1 > 1 ) ;
suppose A31: len s1 <= 1 ; :: thesis:
A32: len s1 >= 0 + 1 by ;
A33: now :: thesis: 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
let n be Nat; :: thesis: ( n + 1 = len s1 implies 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 )

set p = the Permutation of (Seg n);
assume n + 1 = len s1 ; :: thesis: 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

then n + 1 = 1 by ;
then A34: n = 0 ;
take p = the Permutation of (Seg n); :: thesis: 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

let H1 be StableSubgroup of G1; :: thesis: 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

let H2 be StableSubgroup of G2; :: thesis: 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

let N1 be normal StableSubgroup of H1; :: thesis: 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

let N2 be normal StableSubgroup of H2; :: thesis: 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

let i, j be Nat; :: thesis: ( 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )
assume that
A35: ( 1 <= i & i <= n ) and
j = p . i ; :: thesis: ( H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )
assume that
H1 = s1 . i and
H2 = s2 . j ; :: thesis: ( N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )
assume that
N1 = s1 . (i + 1) and
N2 = s2 . (j + 1) ; :: thesis: H1 ./. N1,H2 ./. N2 are_isomorphic
thus H1 ./. N1,H2 ./. N2 are_isomorphic by ; :: thesis: verum
end;
A36: the_series_of_quotients_of s1 = {} by ;
now :: thesis: not len s2 <> 1
assume A37: len s2 <> 1 ; :: thesis: contradiction
len s2 >= 0 + 1 by ;
then len s2 > 1 by ;
then (len ) + 1 > 0 + 1 by Def33;
hence contradiction by A30, A36; :: thesis: verum
end;
then len s1 = len s2 by ;
hence s1 is_equivalent_with s2 by A33; :: thesis: verum
end;
suppose A38: len s1 > 1 ; :: thesis:
then A39: len s1 = () + 1 by Def33;
A41: now :: thesis: for n being Nat st n + 1 = len s1 holds
ex p9 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 = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds
H1 ./. N1,H2 ./. N2 are_isomorphic
let n be Nat; :: thesis: ( n + 1 = len s1 implies ex p9 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 = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds
H1 ./. N1,H2 ./. N2 are_isomorphic )

assume A42: n + 1 = len s1 ; :: thesis: ex p9 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 = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds
H1 ./. N1,H2 ./. N2 are_isomorphic

then A43: dom = Seg n by ;
then reconsider p9 = p " as Permutation of (Seg n) ;
take p9 = p9; :: thesis: 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 = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds
H1 ./. N1,H2 ./. N2 are_isomorphic

let H1 be StableSubgroup of G1; :: thesis: 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 = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds
H1 ./. N1,H2 ./. N2 are_isomorphic

let H2 be StableSubgroup of G2; :: thesis: 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 = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds
H1 ./. N1,H2 ./. N2 are_isomorphic

let N1 be normal StableSubgroup of H1; :: thesis: for N2 being normal StableSubgroup of H2
for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds
H1 ./. N1,H2 ./. N2 are_isomorphic

let N2 be normal StableSubgroup of H2; :: thesis: for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds
H1 ./. N1,H2 ./. N2 are_isomorphic

let i, j be Nat; :: thesis: ( 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )
assume ( 1 <= i & i <= n ) ; :: thesis: ( j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )
then A44: i in dom by A43;
assume A45: j = p9 . i ; :: thesis: ( H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )
assume that
A46: H1 = s1 . i and
A47: H2 = s2 . j ; :: thesis: ( N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )
assume that
A48: N1 = s1 . (i + 1) and
A49: N2 = s2 . (j + 1) ; :: thesis: H1 ./. N1,H2 ./. N2 are_isomorphic
i in dom p9 by ;
then j in rng p9 by ;
then j in Seg n ;
then j in dom by ;
then A50: (the_series_of_quotients_of s2) . j = H2 ./. N2 by ;
(the_series_of_quotients_of s1) . i = H1 ./. N1 by ;
hence H1 ./. N1,H2 ./. N2 are_isomorphic by A29, A44, A45, A50; :: thesis: verum
end;
len s1 = len s2 by ;
hence s1 is_equivalent_with s2 by A41; :: thesis: verum
end;
end;