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

for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 & s2 is jordan_holder & len s1 > len s2 holds

ex i being Nat st

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) )

let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 & s2 is jordan_holder & len s1 > len s2 holds

ex i being Nat st

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) )

let s1, s2 be CompositionSeries of G; :: thesis: ( s1 is_finer_than s2 & s2 is jordan_holder & len s1 > len s2 implies ex i being Nat st

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) ) )

assume A1: s1 is_finer_than s2 ; :: thesis: ( not s2 is jordan_holder or not len s1 > len s2 or ex i being Nat st

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) ) )

assume A2: s2 is jordan_holder ; :: thesis: ( not len s1 > len s2 or ex i being Nat st

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) ) )

assume A3: len s1 > len s2 ; :: thesis: ex i being Nat st

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) )

then not s1 is strictly_decreasing by A1, A2;

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

A4: i in dom s1 and

A5: i + 1 in dom s1 and

A6: ( H1 = s1 . i & N1 = s1 . (i + 1) & H1 ./. N1 is trivial ) ;

i + 1 in Seg (len s1) by A5, FINSEQ_1:def 3;

then A7: i + 1 <= len s1 by FINSEQ_1:1;

0 + 1 <= i + 1 by XREAL_1:6;

then A8: 1 <= len s1 by A7, XXREAL_0:2;

for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 & s2 is jordan_holder & len s1 > len s2 holds

ex i being Nat st

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) )

let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 & s2 is jordan_holder & len s1 > len s2 holds

ex i being Nat st

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) )

let s1, s2 be CompositionSeries of G; :: thesis: ( s1 is_finer_than s2 & s2 is jordan_holder & len s1 > len s2 implies ex i being Nat st

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) ) )

assume A1: s1 is_finer_than s2 ; :: thesis: ( not s2 is jordan_holder or not len s1 > len s2 or ex i being Nat st

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) ) )

assume A2: s2 is jordan_holder ; :: thesis: ( not len s1 > len s2 or ex i being Nat st

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) ) )

assume A3: len s1 > len s2 ; :: thesis: ex i being Nat st

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) )

then not s1 is strictly_decreasing by A1, A2;

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

A4: i in dom s1 and

A5: i + 1 in dom s1 and

A6: ( H1 = s1 . i & N1 = s1 . (i + 1) & H1 ./. N1 is trivial ) ;

i + 1 in Seg (len s1) by A5, FINSEQ_1:def 3;

then A7: i + 1 <= len s1 by FINSEQ_1:1;

0 + 1 <= i + 1 by XREAL_1:6;

then A8: 1 <= len s1 by A7, XXREAL_0:2;

per cases
( len s1 <= 1 or len s1 > 1 )
;

end;

suppose
len s1 <= 1
; :: thesis: ex i being Nat st

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) )

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) )

then A9:
len s1 = 1
by A8, XXREAL_0:1;

hence ex i being Nat st

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) ) by A1, A2, A3; :: thesis: verum

end;now :: thesis: for i being Nat st i in dom s1 & i + 1 in dom s1 holds

for H1 being StableSubgroup of G

for N1 being normal StableSubgroup of H1 st H1 = s1 . i & N1 = s1 . (i + 1) holds

not H1 ./. N1 is trivial

then
s1 is strictly_decreasing
;for H1 being StableSubgroup of G

for N1 being normal StableSubgroup of H1 st H1 = s1 . i & N1 = s1 . (i + 1) holds

not H1 ./. N1 is trivial

let i be Nat; :: thesis: ( i in dom s1 & i + 1 in dom s1 implies for H1 being StableSubgroup of G

for N1 being normal StableSubgroup of H1 st H1 = s1 . i & N1 = s1 . (i + 1) holds

not H1 ./. N1 is trivial )

assume i in dom s1 ; :: thesis: ( i + 1 in dom s1 implies for H1 being StableSubgroup of G

for N1 being normal StableSubgroup of H1 st H1 = s1 . i & N1 = s1 . (i + 1) holds

not H1 ./. N1 is trivial )

then i in Seg 1 by A9, FINSEQ_1:def 3;

then A10: i = 1 by FINSEQ_1:2, TARSKI:def 1;

assume A11: i + 1 in dom s1 ; :: thesis: for H1 being StableSubgroup of G

for N1 being normal StableSubgroup of H1 st H1 = s1 . i & N1 = s1 . (i + 1) holds

not H1 ./. N1 is trivial

let H1 be StableSubgroup of G; :: thesis: for N1 being normal StableSubgroup of H1 st H1 = s1 . i & N1 = s1 . (i + 1) holds

not H1 ./. N1 is trivial

let N1 be normal StableSubgroup of H1; :: thesis: ( H1 = s1 . i & N1 = s1 . (i + 1) implies not H1 ./. N1 is trivial )

assume H1 = s1 . i ; :: thesis: ( N1 = s1 . (i + 1) implies not H1 ./. N1 is trivial )

assume N1 = s1 . (i + 1) ; :: thesis: not H1 ./. N1 is trivial

assume H1 ./. N1 is trivial ; :: thesis: contradiction

2 in Seg 1 by A9, A10, A11, FINSEQ_1:def 3;

hence contradiction by FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

end;for N1 being normal StableSubgroup of H1 st H1 = s1 . i & N1 = s1 . (i + 1) holds

not H1 ./. N1 is trivial )

assume i in dom s1 ; :: thesis: ( i + 1 in dom s1 implies for H1 being StableSubgroup of G

for N1 being normal StableSubgroup of H1 st H1 = s1 . i & N1 = s1 . (i + 1) holds

not H1 ./. N1 is trivial )

then i in Seg 1 by A9, FINSEQ_1:def 3;

then A10: i = 1 by FINSEQ_1:2, TARSKI:def 1;

assume A11: i + 1 in dom s1 ; :: thesis: for H1 being StableSubgroup of G

for N1 being normal StableSubgroup of H1 st H1 = s1 . i & N1 = s1 . (i + 1) holds

not H1 ./. N1 is trivial

let H1 be StableSubgroup of G; :: thesis: for N1 being normal StableSubgroup of H1 st H1 = s1 . i & N1 = s1 . (i + 1) holds

not H1 ./. N1 is trivial

let N1 be normal StableSubgroup of H1; :: thesis: ( H1 = s1 . i & N1 = s1 . (i + 1) implies not H1 ./. N1 is trivial )

assume H1 = s1 . i ; :: thesis: ( N1 = s1 . (i + 1) implies not H1 ./. N1 is trivial )

assume N1 = s1 . (i + 1) ; :: thesis: not H1 ./. N1 is trivial

assume H1 ./. N1 is trivial ; :: thesis: contradiction

2 in Seg 1 by A9, A10, A11, FINSEQ_1:def 3;

hence contradiction by FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

hence ex i being Nat st

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) ) by A1, A2, A3; :: thesis: verum

suppose A12:
len s1 > 1
; :: thesis: ex i being Nat st

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) )

( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) )

take
i
; :: thesis: ( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ) )

A13: (i + 1) - 1 <= (len s1) - 1 by A7, XREAL_1:9;

i in Seg (len s1) by A4, FINSEQ_1:def 3;

then A14: 1 <= i by FINSEQ_1:1;

len s1 = (len (the_series_of_quotients_of s1)) + 1 by A12, Def33;

then i in Seg (len (the_series_of_quotients_of s1)) by A14, A13;

hence A15: i in dom (the_series_of_quotients_of s1) by FINSEQ_1:def 3; :: thesis: for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial

let H be GroupWithOperators of O; :: thesis: ( H = (the_series_of_quotients_of s1) . i implies H is trivial )

assume H = (the_series_of_quotients_of s1) . i ; :: thesis: H is trivial

hence H is trivial by A6, A12, A15, Def33; :: thesis: verum

end;H is trivial ) )

A13: (i + 1) - 1 <= (len s1) - 1 by A7, XREAL_1:9;

i in Seg (len s1) by A4, FINSEQ_1:def 3;

then A14: 1 <= i by FINSEQ_1:1;

len s1 = (len (the_series_of_quotients_of s1)) + 1 by A12, Def33;

then i in Seg (len (the_series_of_quotients_of s1)) by A14, A13;

hence A15: i in dom (the_series_of_quotients_of s1) by FINSEQ_1:def 3; :: thesis: for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial

let H be GroupWithOperators of O; :: thesis: ( H = (the_series_of_quotients_of s1) . i implies H is trivial )

assume H = (the_series_of_quotients_of s1) . i ; :: thesis: H is trivial

hence H is trivial by A6, A12, A15, Def33; :: thesis: verum