let O be set ; :: thesis:
let G be GroupWithOperators of O; :: thesis:
let s1 be CompositionSeries of G; :: thesis:
assume A1: len s1 > 1 ; :: thesis:

A2: now :: thesis:

assume A3: s1 is jordan_holder ; :: thesis:
assume ex i being Nat st
( i in dom (the_series_of_quotients_of s1) & (the_series_of_quotients_of s1) . i is not strict simple GroupWithOperators of O ) ; :: thesis:
then consider i being Nat such that
A4: i in dom (the_series_of_quotients_of s1) and
A5: (the_series_of_quotients_of s1) . i is not strict simple GroupWithOperators of O ;
A6: i in Seg (len (the_series_of_quotients_of s1)) by A4, FINSEQ_1:def 3;
then A7: i <= len (the_series_of_quotients_of s1) by FINSEQ_1:1;
len s1 = (len (the_series_of_quotients_of s1)) + 1 by A1, Def33;
then A8: i + 1 <= len s1 by A7, XREAL_1:6;
0 + 1 <= i + 1 by XREAL_1:6;
then i + 1 in Seg (len s1) by A8;
then A10: i + 1 in dom s1 by FINSEQ_1:def 3;
0 + (len (the_series_of_quotients_of s1)) < 1 + (len (the_series_of_quotients_of s1)) by XREAL_1:6;
then A11: len (the_series_of_quotients_of s1) < len s1 by A1, Def33;
then A12: i <= len s1 by A7, XXREAL_0:2;
1 <= i by A6, FINSEQ_1:1;
then i in Seg (len s1) by A12;
then A13: 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 G by A10, FINSEQ_2:11;
reconsider H1 = H1, N1 = N1 as strict StableSubgroup of G by Def11;
reconsider N1 = N1 as strict normal StableSubgroup of H1 by A13, A10, Def28;
A14: H1 ./. N1 is not strict simple GroupWithOperators of O by A1, A4, A5, Def33;

per cases by A14, Def13;

suppose A15: H1 ./. N1 is trivial ; :: thesis:

s1 is strictly_decreasing by A3;
hence contradiction by A13, A10, A15; :: thesis:

end;

suppose ex H being strict normal StableSubgroup of H1 ./. N1 st
( H <> (Omega). (H1 ./. N1) & H <> (1). (H1 ./. N1) ) ; :: thesis:

then consider H being strict normal StableSubgroup of H1 ./. N1 such that
A16: H <> (Omega). (H1 ./. N1) and
A17: H <> (1). (H1 ./. N1) ;
N1 = Ker (nat_hom N1) by Th48;
then consider N2 being strict StableSubgroup of H1 such that
A18: the carrier of N2 = (nat_hom N1) " the carrier of H and
A19: ( H is normal implies ( N1 is normal StableSubgroup of N2 & N2 is normal ) ) by Th78;
A20: N2 is strict StableSubgroup of G by Th11;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A21: ( 1 <= i & not s1 is empty ) by A1, A6, FINSEQ_1:1;
reconsider N2 = N2 as Element of the_stable_subgroups_of G by A20, Def11;
set s2 = Ins (s1,i,N2);
A22: len (Ins (s1,i,N2)) = (len s1) + 1 by FINSEQ_5:69;
then A23: s1 <> Ins (s1,i,N2) ;

A24: now :: thesis:

let j be Nat; :: thesis:
assume j in dom (Ins (s1,i,N2)) ; :: thesis:
then A26: j in Seg (len (Ins (s1,i,N2))) by FINSEQ_1:def 3;
then A27: 1 <= j by FINSEQ_1:1;
A28: j <= len (Ins (s1,i,N2)) by A26, FINSEQ_1:1;
( j < i or j = i or j > i ) by XXREAL_0:1;
then ( j + 1 <= i or j = i or j >= i + 1 ) by NAT_1:13;
then A29: ( (j + 1) - 1 <= i - 1 or j = i or j >= i + 1 ) by XREAL_1:9;
assume j + 1 in dom (Ins (s1,i,N2)) ; :: thesis:
then A31: j + 1 in Seg (len (Ins (s1,i,N2))) by FINSEQ_1:def 3;
then A32: 1 <= j + 1 by FINSEQ_1:1;
A33: j + 1 <= len (Ins (s1,i,N2)) by A31, FINSEQ_1:1;
let H19, H29 be StableSubgroup of G; :: thesis:
assume A34: H19 = (Ins (s1,i,N2)) . j ; :: thesis:
assume A35: H29 = (Ins (s1,i,N2)) . (j + 1) ; :: thesis:

per cases by A29, XXREAL_0:1;

suppose A36: j <= i - 1 ; :: thesis:

A37: Seg (len (s1 | i)) = Seg i by A11, A7, FINSEQ_1:59, XXREAL_0:2;
A38: dom (s1 | i) c= dom s1 by RELAT_1:60;
(- 1) + i < 0 + i by XREAL_1:6;
then j <= i by A36, XXREAL_0:2;
then j in Seg (len (s1 | i)) by A27, A37;
then A39: j in dom (s1 | i) by FINSEQ_1:def 3;
j + 1 <= (i - 1) + 1 by A36, XREAL_1:6;
then j + 1 in Seg (len (s1 | i)) by A32, A37;
then A40: j + 1 in dom (s1 | i) by FINSEQ_1:def 3;
A41: (Ins (s1,i,N2)) . (j + 1) = s1 . (j + 1) by A40, FINSEQ_5:72;
(Ins (s1,i,N2)) . j = s1 . j by A39, FINSEQ_5:72;
hence H29 is normal StableSubgroup of H19 by A34, A35, A38, A39, A40, A41, Def28; :: thesis:

end;

suppose A42: j = i ; :: thesis:

then A43: j in Seg i by A27;
Seg (len (s1 | i)) = Seg i by A11, A7, FINSEQ_1:59, XXREAL_0:2;
then A44: j in dom (s1 | i) by A43, FINSEQ_1:def 3;
A46: (Ins (s1,i,N2)) . j = s1 . j by A44, FINSEQ_5:72;
(Ins (s1,i,N2)) . (j + 1) = N2 by A11, A7, A42, FINSEQ_5:73, XXREAL_0:2;
hence H29 is normal StableSubgroup of H19 by A19, A34, A35, A42, A46; :: thesis:

end;

suppose A47: j = i + 1 ; :: thesis:

then A48: H19 = N2 by A34, A11, A7, FINSEQ_5:73, XXREAL_0:2;
H29 = s1 . (i + 1) by A35, A47, A8, FINSEQ_5:74;
hence H29 is normal StableSubgroup of H19 by A19, A48; :: thesis:

end;

suppose A50: i + 1 < j ; :: thesis:

set j9 = j - 1;
0 + 1 <= i + 1 by XREAL_1:6;
then A51: 0 + 1 < j by A50, XXREAL_0:2;
then A52: (0 + 1) - 1 < j - 1 by XREAL_1:9;
then reconsider j9 = j - 1 as Element of NAT by INT_1:3;
A53: j - 1 <= (len (Ins (s1,i,N2))) - 1 by A28, XREAL_1:9;
0 + 1 <= j9 by A52, NAT_1:13;
then A54: j9 in dom s1 by A22, A53, FINSEQ_3:25;
(i + 1) + 1 <= j by A50, NAT_1:13;
then A55: ((i + 1) + 1) - 1 <= j - 1 by XREAL_1:9;
0 + j9 < 1 + j9 by XREAL_1:6;
then A56: i + 1 <= j9 + 1 by A55, XXREAL_0:2;
A57: (j + 1) - 1 <= (len (Ins (s1,i,N2))) - 1 by A33, XREAL_1:9;
then A58: j9 + 1 in dom s1 by A22, A51, FINSEQ_3:25;
A59: (Ins (s1,i,N2)) . (j + 1) = s1 . (j9 + 1) by A22, A56, A57, FINSEQ_5:74;
(Ins (s1,i,N2)) . j = (Ins (s1,i,N2)) . (j9 + 1)
.= s1 . j9 by A22, A55, A53, FINSEQ_5:74 ;
hence H29 is normal StableSubgroup of H19 by A34, A35, A54, A58, A59, Def28; :: thesis:

end;

end;

end;

A63: (Ins (s1,i,N2)) . (len (Ins (s1,i,N2))) = (Ins (s1,i,N2)) . ((len s1) + 1) by FINSEQ_5:69
.= s1 . (len s1) by A8, FINSEQ_5:74
.= (1). G by Def28 ;
(Ins (s1,i,N2)) . 1 = s1 . 1 by A21, FINSEQ_5:75
.= (Omega). G by Def28 ;
then reconsider s2 = Ins (s1,i,N2) as CompositionSeries of G by A63, A24, Def28;

now :: thesis:

let j be Nat; :: thesis:
assume j in dom s2 ; :: thesis:
then A65: j in Seg (len s2) by FINSEQ_1:def 3;
then A66: 1 <= j by FINSEQ_1:1;
( j < i or j = i or j > i ) by XXREAL_0:1;
then ( j + 1 <= i or j = i or j >= i + 1 ) by NAT_1:13;
then A67: ( (j + 1) - 1 <= i - 1 or j = i or j >= i + 1 ) by XREAL_1:9;
assume j + 1 in dom s2 ; :: thesis:
then A69: j + 1 in Seg (len s2) by FINSEQ_1:def 3;
then A70: 1 <= j + 1 by FINSEQ_1:1;
A71: j + 1 <= len s2 by A69, FINSEQ_1:1;
let H19 be StableSubgroup of G; :: thesis:
let N19 be normal StableSubgroup of H19; :: thesis:
assume A72: H19 = s2 . j ; :: thesis:
A73: j <= len s2 by A65, FINSEQ_1:1;
A74: s1 is strictly_decreasing by A3;
assume A75: N19 = s2 . (j + 1) ; :: thesis:

per cases by A67, XXREAL_0:1;

suppose A76: j <= i - 1 ; :: thesis:

Seg (len (s1 | i)) = Seg i by A11, A7, FINSEQ_1:59, XXREAL_0:2;
then S: dom (s1 | i) = Seg i by FINSEQ_1:def 3;
A78: dom (s1 | i) c= dom s1 by RELAT_1:60;
(- 1) + i < 0 + i by XREAL_1:6;
then j <= i by A76, XXREAL_0:2;
then A79: j in dom (s1 | i) by A66, S;
j + 1 <= (i - 1) + 1 by A76, XREAL_1:6;
then A80: j + 1 in dom (s1 | i) by A70, S;
then A81: s2 . (j + 1) = s1 . (j + 1) by FINSEQ_5:72;
s2 . j = s1 . j by A79, FINSEQ_5:72;
hence not H19 ./. N19 is trivial by A72, A75, A74, A78, A79, A80, A81; :: thesis:

end;

suppose A82: j = i ; :: thesis:

then A83: j in Seg i by A66;
Seg (len (s1 | i)) = Seg i by A11, A7, FINSEQ_1:59, XXREAL_0:2;
then A84: j in dom (s1 | i) by A83, FINSEQ_1:def 3;
A85: s2 . (j + 1) = N2 by A82, A11, A7, FINSEQ_5:73, XXREAL_0:2;
reconsider N2 = N2 as normal StableSubgroup of H1 by A19;
A87: s2 . j = s1 . j by A84, FINSEQ_5:72;

now :: thesis:

assume H19 ./. N19 is trivial ; :: thesis:
then H1 = N2 by A72, A75, A82, A85, A87, Th76;
hence contradiction by A16, A18, Th80; :: thesis:

end;

hence not H19 ./. N19 is trivial ; :: thesis:

end;

suppose A88: j = i + 1 ; :: thesis:

then A89: H19 = N2 by A72, A11, A7, FINSEQ_5:73, XXREAL_0:2;
A91: N19 = s1 . (i + 1) by A8, FINSEQ_5:74, A75, A88;

now :: thesis:

assume H19 ./. N19 is trivial ; :: thesis:
then the carrier of N1 = (nat_hom N1) " the carrier of H by A18, A89, A91, Th76;
hence contradiction by A17, Th81; :: thesis:

end;

hence not H19 ./. N19 is trivial ; :: thesis:

end;

suppose A92: i + 1 < j ; :: thesis:

set j9 = j - 1;
A93: 0 + 1 <= i + 1 by XREAL_1:6;
then 0 + 1 < j by A92, XXREAL_0:2;
then A94: (0 + 1) - 1 < j - 1 by XREAL_1:9;
then reconsider j9 = j - 1 as Element of NAT by INT_1:3;
A95: (j + 1) - 1 <= (len s2) - 1 by A71, XREAL_1:9;
(i + 1) + 1 <= j by A92, NAT_1:13;
then A96: ((i + 1) + 1) - 1 <= j - 1 by XREAL_1:9;
1 <= j9 + 1 by A92, A93, XXREAL_0:2;
then A97: j9 + 1 in dom s1 by A22, A95, FINSEQ_3:25;
0 + j9 < 1 + j9 by XREAL_1:6;
then A98: i + 1 <= j9 + 1 by A96, XXREAL_0:2;
A99: s2 . (j + 1) = s1 . (j9 + 1) by A22, A98, A95, FINSEQ_5:74;
A100: j - 1 <= (len s2) - 1 by A73, XREAL_1:9;
0 + 1 <= j9 by A94, NAT_1:13;
then A101: j9 in dom s1 by A22, A100, FINSEQ_3:25;
s2 . j = s2 . (j9 + 1)
.= s1 . j9 by A22, A96, A100, FINSEQ_5:74 ;
hence not H19 ./. N19 is trivial by A72, A75, A74, A101, A97, A99; :: thesis:

end;

end;

end;

then A102: s2 is strictly_decreasing ;
( (dom s2) \ {(i + 1)} c= dom s2 & s1 = Del (s2,(i + 1)) ) by A13, Lm43, XBOOLE_1:36;
then s2 is_finer_than s1 ;
hence contradiction by A3, A23, A102; :: thesis:

end;

end;

end;

now :: thesis:

assume A103: for i being Nat st i in dom (the_series_of_quotients_of s1) holds
(the_series_of_quotients_of s1) . i is strict simple GroupWithOperators of O ; :: thesis:
assume A104: not s1 is jordan_holder ; :: thesis:

per cases by A104;

suppose not s1 is strictly_decreasing ; :: thesis:

then ex i being Nat st
( i in dom s1 & i + 1 in dom s1 & ex H1 being StableSubgroup of G ex N1 being normal StableSubgroup of H1 st
( H1 = s1 . i & N1 = s1 . (i + 1) & H1 ./. N1 is trivial ) ) ;
then consider i being Nat, H1 being StableSubgroup of G, N1 being normal StableSubgroup of H1 such that
A105: i in dom s1 and
A106: i + 1 in dom s1 and
A107: ( H1 = s1 . i & N1 = s1 . (i + 1) ) and
A108: H1 ./. N1 is trivial ;
A109: i + 1 <= len s1 by FINSEQ_3:25, A106;
A110: 1 <= i by A105, FINSEQ_3:25;
then 1 + 1 <= i + 1 by XREAL_1:6;
then 1 + 1 <= len s1 by A109, XXREAL_0:2;
then A111: len s1 > 1 by NAT_1:13;
then (len (the_series_of_quotients_of s1)) + 1 = len s1 by Def33;
then len (the_series_of_quotients_of s1) = (len s1) - 1 ;
then (i + 1) - 1 <= len (the_series_of_quotients_of s1) by A109, XREAL_1:9;
then i in Seg (len (the_series_of_quotients_of s1)) by A110;
then A112: i in dom (the_series_of_quotients_of s1) by FINSEQ_1:def 3;
then (the_series_of_quotients_of s1) . i = H1 ./. N1 by A107, A111, Def33;
then H1 ./. N1 is strict simple GroupWithOperators of O by A103, A112;
hence contradiction by A108, Def13; :: thesis:

end;

suppose ex s2 being CompositionSeries of G st
( s2 <> s1 & s2 is strictly_decreasing & s2 is_finer_than s1 ) ; :: thesis:

then consider s2 being CompositionSeries of G such that
A113: s2 <> s1 and
A114: s2 is strictly_decreasing and
A115: s2 is_finer_than s1 ;
consider i, j being Nat such that
A116: i in dom s1 and
A117: i in dom s2 and
A118: i + 1 in dom s1 and
A119: i + 1 in dom s2 and
A120: ( j in dom s2 & i + 1 < j ) and
A121: s1 . i = s2 . i and
A122: s1 . (i + 1) <> s2 . (i + 1) and
A123: s1 . (i + 1) = s2 . j by A1, A113, A114, A115, Th100;
reconsider H1 = s1 . i, H2 = s1 . (i + 1), H = s2 . (i + 1) as Element of the_stable_subgroups_of G by A116, A118, A119, FINSEQ_2:11;
reconsider H1 = H1, H2 = H2, H = H as strict StableSubgroup of G by Def11;
reconsider H2 = H2 as strict normal StableSubgroup of H1 by A116, A118, Def28;
reconsider H = H as strict normal StableSubgroup of H1 by A117, A119, A121, Def28;
reconsider H29 = H2 as normal StableSubgroup of H by A119, A120, A123, Th40, Th101;
reconsider J = H ./. H29 as strict normal StableSubgroup of H1 ./. H2 by Th44;

A124: now :: thesis:

assume J = (Omega). (H1 ./. H2) ; :: thesis:
then A125: the carrier of H = union (Cosets H2) by Th22;
then A126: H = H1 by Lm4, Th22;
then reconsider H1 = H1 as strict normal StableSubgroup of H ;
H1 = (Omega). H by A125, Lm4, Th22;
then H ./. H1 is trivial by Th57;
hence contradiction by A114, A117, A119, A121, A126; :: thesis:

end;

reconsider H3 = HGrWOpStr(# the carrier of H2, the multF of H2, the action of H2 #) as strict normal StableSubgroup of H by A119, A120, A123, Th40, Th101;

now :: thesis:

assume J = (1). (H1 ./. H2) ; :: thesis:
then union (Cosets H3) = union {(1_ (H1 ./. H2))} by Def8;
then the carrier of H = union {(1_ (H1 ./. H2))} by Th22;
then the carrier of H = 1_ (H1 ./. H2) by ZFMISC_1:25;
then the carrier of H = carr H2 by Th43;
hence contradiction by A122, Lm4; :: thesis:

end;

then A127: H1 ./. H2 is not simple GroupWithOperators of O by A124, Def13;
i + 1 in Seg (len s1) by A118, FINSEQ_1:def 3;
then A128: i + 1 <= len s1 by FINSEQ_1:1;
i in Seg (len s1) by A116, FINSEQ_1:def 3;
then A129: 1 <= i by FINSEQ_1:1;
then 1 + 1 <= i + 1 by XREAL_1:6;
then 1 + 1 <= len s1 by A128, XXREAL_0:2;
then A130: len s1 > 1 by NAT_1:13;
then (len (the_series_of_quotients_of s1)) + 1 = len s1 by Def33;
then len (the_series_of_quotients_of s1) = (len s1) - 1 ;
then (i + 1) - 1 <= len (the_series_of_quotients_of s1) by A128, XREAL_1:9;
then i in Seg (len (the_series_of_quotients_of s1)) by A129;
then A131: i in dom (the_series_of_quotients_of s1) by FINSEQ_1:def 3;
then (the_series_of_quotients_of s1) . i = H1 ./. H2 by A130, Def33;
hence contradiction by A103, A127, A131; :: thesis:

end;

end;

end;

hence ( s1 is jordan_holder iff for i being Nat st i in dom (the_series_of_quotients_of s1) holds
(the_series_of_quotients_of s1) . i is strict simple GroupWithOperators of O ) by A2; :: thesis: