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 A1: ( not s1 is empty & not s2 is empty ) ; :: thesis:
set f1 = the_series_of_quotients_of s1;
set f2 = the_series_of_quotients_of s2;

hereby :: thesis:

assume A2: s1 is_equivalent_with s2 ; :: thesis:
then A3: len s1 = len s2 by Def35;

per cases ;

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

consider p being Permutation of (dom (the_series_of_quotients_of s1));
take p = p; :: thesis:
reconsider fs1 = the_series_of_quotients_of s1, fs2 = the_series_of_quotients_of s2 as FinSequence ;
A5: fs1 = {} by A4, Def36;
A6: fs2 = {} by A3, A4, Def36;
reconsider pf = p as Permutation of (dom fs1) ;
A7: len (the_series_of_quotients_of s1) = len (the_series_of_quotients_of s2) by A4, A6, Def36;
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 by A5;
hence the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O by A7, Def37; :: thesis:

end;

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

then A9: (len s1) - 1 > 1 - 1 by XREAL_1:11;
set n = (len s1) - 1;
(len s1) - 1 in NAT by A9, INT_1:16;
then reconsider n = (len s1) - 1 as Nat ;
n + 1 = len s1 ;
then consider p being Permutation of (Seg n) such that
A10: 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 A2, Def35;
A11: len s1 = (len (the_series_of_quotients_of s1)) + 1 by A8, Def36;
then dom (the_series_of_quotients_of s1) = Seg n by FINSEQ_1:def 3;
then reconsider p' = p " as Permutation of (dom (the_series_of_quotients_of s1)) ;
take p' = p'; :: thesis:
reconsider fs1 = the_series_of_quotients_of s1, fs2 = the_series_of_quotients_of s2 as FinSequence ;
reconsider pf = p' as Permutation of (dom fs1) ;
A12: len s2 = (len (the_series_of_quotients_of s2)) + 1 by A3, A8, Def36;
A13: pf " = p by FUNCT_1:65;

now

let H1', H2' be GroupWithOperators of O; :: thesis:
let i, j be Nat; :: thesis:
assume A14: i in dom fs1 ; :: thesis:
assume A15: j = (pf " ) . i ; :: thesis:
assume A16: ( H1' = fs1 . i & H2' = fs2 . j ) ; :: thesis:
set H1 = s1 . i;
set H2 = s2 . j;
set N1 = s1 . (i + 1);
set N2 = s2 . (j + 1);
A17: i in Seg (len fs1) by A14, FINSEQ_1:def 3;
then A18: ( 1 <= i & i <= len fs1 ) by FINSEQ_1:3;
0 + (len fs1) < 1 + (len fs1) by XREAL_1:8;
then i <= len s1 by A11, A18, XXREAL_0:2;
then i in Seg (len s1) by A18, FINSEQ_1:3;
then A19: i in dom s1 by FINSEQ_1:def 3;
0 + i < 1 + i by XREAL_1:8;
then A20: 1 <= i + 1 by A18, XXREAL_0:2;
i + 1 <= (len fs1) + 1 by A18, XREAL_1:8;
then i + 1 in Seg (len s1) by A11, A20;
then A21: i + 1 in dom s1 by FINSEQ_1:def 3;
i in dom p by A11, A17, FUNCT_2:def 1;
then A22: j in rng p by A13, A15, FUNCT_1:12;
then A23: j in Seg (len (the_series_of_quotients_of s2)) by A3, A12;
A24: ( 1 <= j & j <= len fs2 ) by A3, A12, A22, FINSEQ_1:3;
0 + (len fs2) < 1 + (len fs2) by XREAL_1:8;
then j <= len s2 by A12, A24, XXREAL_0:2;
then j in Seg (len s2) by A24, FINSEQ_1:3;
then A25: j in dom s2 by FINSEQ_1:def 3;
0 + j < 1 + j by XREAL_1:8;
then A26: 1 <= j + 1 by A24, XXREAL_0:2;
j + 1 <= (len fs2) + 1 by A24, XREAL_1:8;
then j + 1 in Seg (len s2) by A12, A26;
then A27: j + 1 in dom s2 by FINSEQ_1:def 3;
reconsider H1 = s1 . i, N1 = s1 . (i + 1) as Element of the_stable_subgroups_of G1 by A19, A21, FINSEQ_2:13;
reconsider H1 = H1, N1 = N1 as StableSubgroup of G1 by Def11;
reconsider N1 = N1 as normal StableSubgroup of H1 by A19, A21, Def31;
reconsider H2 = s2 . j, N2 = s2 . (j + 1) as Element of the_stable_subgroups_of G2 by A25, A27, FINSEQ_2:13;
reconsider H2 = H2, N2 = N2 as StableSubgroup of G2 by Def11;
reconsider N2 = N2 as normal StableSubgroup of H2 by A25, A27, Def31;
A28: j in dom fs2 by A23, FINSEQ_1:def 3;
dom fs1 = Seg n by A11, FINSEQ_1:def 3;
then ( 1 <= i & i <= n ) by A14, FINSEQ_1:3;
then A29: H1 ./. N1,H2 ./. N2 are_isomorphic by A10, A13, A15;
H2 ./. N2 = H2' by A3, A8, A16, A28, Def36;
hence H1',H2' are_isomorphic by A8, A14, A16, A29, Def36; :: thesis:

end;

hence the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p',O by A3, A11, A12, Def37; :: thesis:

end;

per cases ;

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

len s1 <> 0 by A1;
then len s1 > 0 ;
then A33: len s1 >= 0 + 1 by NAT_1:13;
A34: the_series_of_quotients_of s1 = {} by A32, Def36;

now

assume A35: len s2 <> 1 ; :: thesis:
len s2 <> 0 by A1;
then len s2 > 0 ;
then len s2 >= 0 + 1 by NAT_1:13;
then len s2 > 1 by A35, XXREAL_0:1;
then (len (the_series_of_quotients_of s2)) + 1 > 0 + 1 by Def36;
hence contradiction by A31, A34; :: thesis:

end;

then A36: len s1 = len s2 by A32, A33, XXREAL_0:1;

now

let n be Nat; :: thesis:
assume n + 1 = len s1 ; :: thesis:
then n + 1 = 1 by A32, A33, XXREAL_0:1;
then A37: n = 0 ;
consider p being Permutation of (Seg n);
take p = p; :: 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 A38: ( 1 <= i & i <= n & j = p . i ) ; :: thesis:
assume ( H1 = s1 . i & H2 = s2 . j ) ; :: thesis:
assume ( N1 = s1 . (i + 1) & N2 = s2 . (j + 1) ) ; :: thesis:
thus H1 ./. N1,H2 ./. N2 are_isomorphic by A37, A38; :: thesis:

end;

hence s1 is_equivalent_with s2 by A36, Def35; :: thesis:

end;

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

then A40: ( len s1 = (len (the_series_of_quotients_of s1)) + 1 & ( for i being Nat st i in dom (the_series_of_quotients_of s1) holds
for H1 being StableSubgroup of G1
for N1 being normal StableSubgroup of H1 st H1 = s1 . i & N1 = s1 . (i + 1) holds
(the_series_of_quotients_of s1) . i = H1 ./. N1 ) ) by Def36;

A41: now

assume len s2 <= 1 ; :: thesis:
then the_series_of_quotients_of s2 = {} by Def36;
then len (the_series_of_quotients_of s2) = 0 ;
hence contradiction by A31, A39, A40; :: thesis:

end;

then A42: len s1 = len s2 by A31, A40, Def36;

now

let n be Nat; :: thesis:
assume A43: n + 1 = len s1 ; :: thesis:
then A44: dom (the_series_of_quotients_of s1) = Seg n by A40, FINSEQ_1:def 3;
then reconsider p' = p " as Permutation of (Seg n) ;
take p' = p'; :: 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 A45: i in dom (the_series_of_quotients_of s1) by A44, FINSEQ_1:3;
then A46: i in dom p' by FUNCT_2:def 1;
assume A47: j = p' . i ; :: thesis:
assume A48: ( H1 = s1 . i & H2 = s2 . j ) ; :: thesis:
assume A49: ( N1 = s1 . (i + 1) & N2 = s2 . (j + 1) ) ; :: thesis:
then A50: (the_series_of_quotients_of s1) . i = H1 ./. N1 by A39, A45, A48, Def36;
j in rng p' by A46, A47, FUNCT_1:12;
then j in Seg n ;
then j in dom (the_series_of_quotients_of s2) by A31, A40, A43, FINSEQ_1:def 3;
then (the_series_of_quotients_of s2) . j = H2 ./. N2 by A41, A48, A49, Def36;
hence H1 ./. N1,H2 ./. N2 are_isomorphic by A30, A45, A47, A50, Def37; :: thesis:

end;

hence s1 is_equivalent_with s2 by A42, Def35; :: thesis:

end;