let O be set ; :: thesis:
let G1, G2 be GroupWithOperators of O; :: thesis:
let s1 be CompositionSeries of G1; :: thesis:
let s2 be CompositionSeries of G2; :: thesis:
assume that
A1: not s1 is empty and
A2: not s2 is empty ; :: thesis:
set f2 = the_series_of_quotients_of s2;
set f1 = the_series_of_quotients_of s1;

hereby :: thesis:

assume A3: s1 is_equivalent_with s2 ; :: thesis:
then A4: len s1 = len s2 ;

per cases ;

suppose A5: len s1 <= 1 ; :: thesis:

end;

suppose A7: len s1 > 1 ; :: thesis:

set n = (len s1) - 1;
(len s1) - 1 > 1 - 1 by A7, XREAL_1:9;
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 = (len (the_series_of_quotients_of s1)) + 1 by A7, Def33;
then dom (the_series_of_quotients_of s1) = Seg n by FINSEQ_1:def 3;
then reconsider p9 = p " as Permutation of (dom (the_series_of_quotients_of s1)) ;
reconsider fs1 = the_series_of_quotients_of s1, fs2 = the_series_of_quotients_of s2 as FinSequence ;
A10: len s2 = (len (the_series_of_quotients_of s2)) + 1 by A4, A7, Def33;
reconsider pf = p9 as Permutation of (dom fs1) ;
take p9 = p9; :: thesis:
A11: pf " = p by FUNCT_1:43;

now :: thesis:

let H19, H29 be GroupWithOperators of O; :: thesis:
let i, j be Nat; :: thesis:
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:
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 A13, FINSEQ_1:1;
then A16: i + 1 <= (len fs1) + 1 by XREAL_1:6;
0 + i < 1 + i by XREAL_1:6;
then 1 <= i + 1 by A14, XXREAL_0:2;
then i + 1 in Seg (len s1) by A9, A16;
then A17: i + 1 in dom s1 by FINSEQ_1:def 3;
assume A18: j = (pf ") . i ; :: thesis:
0 + (len fs1) < 1 + (len fs1) by XREAL_1:6;
then i <= len s1 by A9, A15, XXREAL_0:2;
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 A17, FINSEQ_2:11;
reconsider H1 = H1, N1 = N1 as StableSubgroup of G1 by Def11;
reconsider N1 = N1 as normal StableSubgroup of H1 by A19, A17, Def28;
assume that
A20: H19 = fs1 . i and
A21: H29 = fs2 . j ; :: thesis:
i in dom p by A9, A13, FUNCT_2:def 1;
then A22: j in rng p by A11, A18, FUNCT_1:3;
then A23: 1 <= j by FINSEQ_1:1;
A24: j <= len fs2 by A4, A10, A22, FINSEQ_1:1;
then A25: j + 1 <= (len fs2) + 1 by XREAL_1:6;
0 + j < 1 + j by XREAL_1:6;
then 1 <= j + 1 by A23, XXREAL_0:2;
then j + 1 in Seg (len s2) by A10, A25;
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 A10, A24, XXREAL_0:2;
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 A26, FINSEQ_2:11;
reconsider H2 = H2, N2 = N2 as StableSubgroup of G2 by Def11;
reconsider N2 = N2 as normal StableSubgroup of H2 by A27, A26, Def28;
dom fs1 = Seg n by A9, FINSEQ_1:def 3;
then ( 1 <= i & i <= n ) by A12, FINSEQ_1:1;
then A28: H1 ./. N1,H2 ./. N2 are_isomorphic by A8, A11, A18;
j in Seg (len (the_series_of_quotients_of s2)) 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:

end;

hence the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p9,O by A4, A9, A10; :: thesis:

end;

given p being Permutation of (dom (the_series_of_quotients_of s1)) such that A29: the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O ; :: thesis:
A30: len (the_series_of_quotients_of s1) = len (the_series_of_quotients_of s2) by A29;

per cases ;

suppose A31: len s1 <= 1 ; :: thesis:

A32: len s1 >= 0 + 1 by A1, NAT_1:13;

A33: now :: thesis:

let n be Nat; :: thesis:
set p = the Permutation of (Seg n);
assume n + 1 = len s1 ; :: thesis:
then n + 1 = 1 by A31, A32, XXREAL_0:1;
then A34: n = 0 ;
take p = the Permutation of (Seg n); :: thesis:
let H1 be StableSubgroup of G1; :: thesis:
let H2 be StableSubgroup of G2; :: thesis:
let N1 be normal StableSubgroup of H1; :: thesis:
let N2 be normal StableSubgroup of H2; :: thesis:
let i, j be Nat; :: thesis:
assume that
A35: ( 1 <= i & i <= n ) and
j = p . i ; :: thesis:
assume that
H1 = s1 . i and
H2 = s2 . j ; :: thesis:
assume that
N1 = s1 . (i + 1) and
N2 = s2 . (j + 1) ; :: thesis:
thus H1 ./. N1,H2 ./. N2 are_isomorphic by A34, A35; :: thesis:

end;

A36: the_series_of_quotients_of s1 = {} by A31, Def33;

now :: thesis:

assume A37: len s2 <> 1 ; :: thesis:
len s2 >= 0 + 1 by A2, NAT_1:13;
then len s2 > 1 by A37, XXREAL_0:1;
then (len (the_series_of_quotients_of s2)) + 1 > 0 + 1 by Def33;
hence contradiction by A30, A36; :: thesis:

end;

then len s1 = len s2 by A31, A32, XXREAL_0:1;
hence s1 is_equivalent_with s2 by A33; :: thesis:

end;

suppose A38: len s1 > 1 ; :: thesis:

then A39: len s1 = (len (the_series_of_quotients_of s1)) + 1 by Def33;

A40: now :: thesis:

assume len s2 <= 1 ; :: thesis:
then the_series_of_quotients_of s2 = {} by Def33;
then len (the_series_of_quotients_of s2) = 0 ;
hence contradiction by A30, A38, A39; :: thesis:

end;

A41: now :: thesis:

let n be Nat; :: thesis:
assume A42: n + 1 = len s1 ; :: thesis:
then A43: dom (the_series_of_quotients_of s1) = Seg n by A39, FINSEQ_1:def 3;
then reconsider p9 = p " as Permutation of (Seg n) ;
take p9 = p9; :: thesis:
let H1 be StableSubgroup of G1; :: thesis:
let H2 be StableSubgroup of G2; :: thesis:
let N1 be normal StableSubgroup of H1; :: thesis:
let N2 be normal StableSubgroup of H2; :: thesis:
let i, j be Nat; :: thesis:
assume ( 1 <= i & i <= n ) ; :: thesis:
then A44: i in dom (the_series_of_quotients_of s1) by A43;
assume A45: j = p9 . i ; :: thesis:
assume that
A46: H1 = s1 . i and
A47: H2 = s2 . j ; :: thesis:
assume that
A48: N1 = s1 . (i + 1) and
A49: N2 = s2 . (j + 1) ; :: thesis:
i in dom p9 by A44, FUNCT_2:def 1;
then j in rng p9 by A45, FUNCT_1:3;
then j in Seg n ;
then j in dom (the_series_of_quotients_of s2) by A30, A39, A42, FINSEQ_1:def 3;
then A50: (the_series_of_quotients_of s2) . j = H2 ./. N2 by A40, A47, A49, Def33;
(the_series_of_quotients_of s1) . i = H1 ./. N1 by A38, A44, A46, A48, Def33;
hence H1 ./. N1,H2 ./. N2 are_isomorphic by A29, A44, A45, A50; :: thesis:

end;

len s1 = len s2 by A30, A39, A40, Def33;
hence s1 is_equivalent_with s2 by A41; :: thesis:

end;