let O be set ; :: thesis: for G being GroupWithOperators of O

for s1 being CompositionSeries of G st len s1 > 1 holds

( 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 )

let G be GroupWithOperators of O; :: thesis: for s1 being CompositionSeries of G st len s1 > 1 holds

( 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 )

let s1 be CompositionSeries of G; :: thesis: ( len s1 > 1 implies ( 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 ) )

assume A1: len s1 > 1 ; :: thesis: ( 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 )

(the_series_of_quotients_of s1) . i is strict simple GroupWithOperators of O ) by A2; :: thesis: verum

for s1 being CompositionSeries of G st len s1 > 1 holds

( 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 )

let G be GroupWithOperators of O; :: thesis: for s1 being CompositionSeries of G st len s1 > 1 holds

( 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 )

let s1 be CompositionSeries of G; :: thesis: ( len s1 > 1 implies ( 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 ) )

assume A1: len s1 > 1 ; :: thesis: ( 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 )

A2: now :: thesis: ( s1 is jordan_holder implies 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 )

(the_series_of_quotients_of s1) . i is strict simple GroupWithOperators of O )

assume A3:
s1 is jordan_holder
; :: thesis: 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

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: contradiction

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;

end;(the_series_of_quotients_of s1) . i is strict simple GroupWithOperators of O

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: contradiction

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
( H1 ./. N1 is trivial or ex H being strict normal StableSubgroup of H1 ./. N1 st

( H <> (Omega). (H1 ./. N1) & H <> (1). (H1 ./. N1) ) ) by A14, Def13;

end;

( H <> (Omega). (H1 ./. N1) & H <> (1). (H1 ./. N1) ) ) by A14, Def13;

suppose
ex H being strict normal StableSubgroup of H1 ./. N1 st

( H <> (Omega). (H1 ./. N1) & H <> (1). (H1 ./. N1) ) ; :: thesis: contradiction

( H <> (Omega). (H1 ./. N1) & H <> (1). (H1 ./. N1) ) ; :: thesis: contradiction

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) ;

.= 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;

( (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: verum

end;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: for j being Nat st j in dom (Ins (s1,i,N2)) & j + 1 in dom (Ins (s1,i,N2)) holds

for H19, H29 being StableSubgroup of G st H19 = (Ins (s1,i,N2)) . j & H29 = (Ins (s1,i,N2)) . (j + 1) holds

H29 is normal StableSubgroup of H19

A63: (Ins (s1,i,N2)) . (len (Ins (s1,i,N2))) =
(Ins (s1,i,N2)) . ((len s1) + 1)
by FINSEQ_5:69
for H19, H29 being StableSubgroup of G st H19 = (Ins (s1,i,N2)) . j & H29 = (Ins (s1,i,N2)) . (j + 1) holds

H29 is normal StableSubgroup of H19

let j be Nat; :: thesis: ( j in dom (Ins (s1,i,N2)) & j + 1 in dom (Ins (s1,i,N2)) implies for H19, H29 being StableSubgroup of G st H19 = (Ins (s1,i,N2)) . j & H29 = (Ins (s1,i,N2)) . (j + 1) holds

b_{5} is normal StableSubgroup of b_{4} )

assume j in dom (Ins (s1,i,N2)) ; :: thesis: ( j + 1 in dom (Ins (s1,i,N2)) implies for H19, H29 being StableSubgroup of G st H19 = (Ins (s1,i,N2)) . j & H29 = (Ins (s1,i,N2)) . (j + 1) holds

b_{5} is normal StableSubgroup of b_{4} )

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: for H19, H29 being StableSubgroup of G st H19 = (Ins (s1,i,N2)) . j & H29 = (Ins (s1,i,N2)) . (j + 1) holds

b_{5} is normal StableSubgroup of b_{4}

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: ( H19 = (Ins (s1,i,N2)) . j & H29 = (Ins (s1,i,N2)) . (j + 1) implies b_{3} is normal StableSubgroup of b_{2} )

assume A34: H19 = (Ins (s1,i,N2)) . j ; :: thesis: ( H29 = (Ins (s1,i,N2)) . (j + 1) implies b_{3} is normal StableSubgroup of b_{2} )

assume A35: H29 = (Ins (s1,i,N2)) . (j + 1) ; :: thesis: b_{3} is normal StableSubgroup of b_{2}

end;b

assume j in dom (Ins (s1,i,N2)) ; :: thesis: ( j + 1 in dom (Ins (s1,i,N2)) implies for H19, H29 being StableSubgroup of G st H19 = (Ins (s1,i,N2)) . j & H29 = (Ins (s1,i,N2)) . (j + 1) holds

b

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: for H19, H29 being StableSubgroup of G st H19 = (Ins (s1,i,N2)) . j & H29 = (Ins (s1,i,N2)) . (j + 1) holds

b

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: ( H19 = (Ins (s1,i,N2)) . j & H29 = (Ins (s1,i,N2)) . (j + 1) implies b

assume A34: H19 = (Ins (s1,i,N2)) . j ; :: thesis: ( H29 = (Ins (s1,i,N2)) . (j + 1) implies b

assume A35: H29 = (Ins (s1,i,N2)) . (j + 1) ; :: thesis: b

per cases
( j <= i - 1 or j = i or j = i + 1 or i + 1 < j )
by A29, XXREAL_0:1;

end;

suppose A36:
j <= i - 1
; :: thesis: b_{3} is normal StableSubgroup of b_{2}

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: verum

end;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: verum

suppose A42:
j = i
; :: thesis: b_{3} is normal StableSubgroup of b_{2}

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: verum

end;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: verum

suppose A47:
j = i + 1
; :: thesis: b_{3} is normal StableSubgroup of b_{2}

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: verum

end;H29 = s1 . (i + 1) by A35, A47, A8, FINSEQ_5:74;

hence H29 is normal StableSubgroup of H19 by A19, A48; :: thesis: verum

suppose A50:
i + 1 < j
; :: thesis: b_{3} is normal StableSubgroup of b_{2}

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: verum

end;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: verum

.= 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: for j being Nat st j in dom s2 & j + 1 in dom s2 holds

for H19 being StableSubgroup of G

for N19 being normal StableSubgroup of H19 st H19 = s2 . j & N19 = s2 . (j + 1) holds

not H19 ./. N19 is trivial

then A102:
s2 is strictly_decreasing
;for H19 being StableSubgroup of G

for N19 being normal StableSubgroup of H19 st H19 = s2 . j & N19 = s2 . (j + 1) holds

not H19 ./. N19 is trivial

let j be Nat; :: thesis: ( j in dom s2 & j + 1 in dom s2 implies for H19 being StableSubgroup of G

for N19 being normal StableSubgroup of H19 st H19 = s2 . j & N19 = s2 . (j + 1) holds

not b_{4} ./. b_{5} is trivial )

assume j in dom s2 ; :: thesis: ( j + 1 in dom s2 implies for H19 being StableSubgroup of G

for N19 being normal StableSubgroup of H19 st H19 = s2 . j & N19 = s2 . (j + 1) holds

not b_{4} ./. b_{5} is trivial )

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: for H19 being StableSubgroup of G

for N19 being normal StableSubgroup of H19 st H19 = s2 . j & N19 = s2 . (j + 1) holds

not b_{4} ./. b_{5} is trivial

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: for N19 being normal StableSubgroup of H19 st H19 = s2 . j & N19 = s2 . (j + 1) holds

not b_{3} ./. b_{4} is trivial

let N19 be normal StableSubgroup of H19; :: thesis: ( H19 = s2 . j & N19 = s2 . (j + 1) implies not b_{2} ./. b_{3} is trivial )

assume A72: H19 = s2 . j ; :: thesis: ( N19 = s2 . (j + 1) implies not b_{2} ./. b_{3} is trivial )

A73: j <= len s2 by A65, FINSEQ_1:1;

A74: s1 is strictly_decreasing by A3;

assume A75: N19 = s2 . (j + 1) ; :: thesis: not b_{2} ./. b_{3} is trivial

end;for N19 being normal StableSubgroup of H19 st H19 = s2 . j & N19 = s2 . (j + 1) holds

not b

assume j in dom s2 ; :: thesis: ( j + 1 in dom s2 implies for H19 being StableSubgroup of G

for N19 being normal StableSubgroup of H19 st H19 = s2 . j & N19 = s2 . (j + 1) holds

not b

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: for H19 being StableSubgroup of G

for N19 being normal StableSubgroup of H19 st H19 = s2 . j & N19 = s2 . (j + 1) holds

not b

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: for N19 being normal StableSubgroup of H19 st H19 = s2 . j & N19 = s2 . (j + 1) holds

not b

let N19 be normal StableSubgroup of H19; :: thesis: ( H19 = s2 . j & N19 = s2 . (j + 1) implies not b

assume A72: H19 = s2 . j ; :: thesis: ( N19 = s2 . (j + 1) implies not b

A73: j <= len s2 by A65, FINSEQ_1:1;

A74: s1 is strictly_decreasing by A3;

assume A75: N19 = s2 . (j + 1) ; :: thesis: not b

per cases
( j <= i - 1 or j = i or j = i + 1 or i + 1 < j )
by A67, XXREAL_0:1;

end;

suppose A76:
j <= i - 1
; :: thesis: not b_{2} ./. b_{3} is trivial

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: verum

end;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: verum

suppose A82:
j = i
; :: thesis: not b_{2} ./. b_{3} is trivial

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;

end;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: not H19 ./. N19 is trivial

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

then H1 = N2 by A72, A75, A82, A85, A87, Th76;

hence contradiction by A16, A18, Th80; :: thesis: verum

end;then H1 = N2 by A72, A75, A82, A85, A87, Th76;

hence contradiction by A16, A18, Th80; :: thesis: verum

suppose A88:
j = i + 1
; :: thesis: not b_{2} ./. b_{3} is trivial

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;

end;A91: N19 = s1 . (i + 1) by A8, FINSEQ_5:74, A75, A88;

now :: thesis: not H19 ./. N19 is trivial

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

then the carrier of N1 = (nat_hom N1) " the carrier of H by A18, A89, A91, Th76;

hence contradiction by A17, Th81; :: thesis: verum

end;then the carrier of N1 = (nat_hom N1) " the carrier of H by A18, A89, A91, Th76;

hence contradiction by A17, Th81; :: thesis: verum

suppose A92:
i + 1 < j
; :: thesis: not b_{2} ./. b_{3} is trivial

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: verum

end;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: verum

( (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: verum

now :: thesis: ( ( 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 ) implies s1 is jordan_holder )

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 ) implies s1 is jordan_holder )

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: s1 is jordan_holder

assume A104: not s1 is jordan_holder ; :: thesis: contradiction

end;(the_series_of_quotients_of s1) . i is strict simple GroupWithOperators of O ; :: thesis: s1 is jordan_holder

assume A104: not s1 is jordan_holder ; :: thesis: contradiction

per cases
( not s1 is strictly_decreasing or ex s2 being CompositionSeries of G st

( s2 <> s1 & s2 is strictly_decreasing & s2 is_finer_than s1 ) ) by A104;

end;

( s2 <> s1 & s2 is strictly_decreasing & s2 is_finer_than s1 ) ) by A104;

suppose
not s1 is strictly_decreasing
; :: thesis: contradiction

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: verum

end;( 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: verum

suppose
ex s2 being CompositionSeries of G st

( s2 <> s1 & s2 is strictly_decreasing & s2 is_finer_than s1 ) ; :: thesis: contradiction

( s2 <> s1 & s2 is strictly_decreasing & s2 is_finer_than s1 ) ; :: thesis: contradiction

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;

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: verum

end;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: not J = (Omega). (H1 ./. H2)

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;assume
J = (Omega). (H1 ./. H2)
; :: thesis: contradiction

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: verum

end;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: verum

now :: thesis: not J = (1). (H1 ./. H2)

then A127:
H1 ./. H2 is not simple GroupWithOperators of O
by A124, Def13;assume
J = (1). (H1 ./. H2)
; :: thesis: contradiction

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: verum

end;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: verum

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: verum

(the_series_of_quotients_of s1) . i is strict simple GroupWithOperators of O ) by A2; :: thesis: verum