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 & ( for H being GroupWithOperators of O st H = . 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 & ( for H being GroupWithOperators of O st H = . 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 & ( for H being GroupWithOperators of O st H = . 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 & ( for H being GroupWithOperators of O st H = . 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 & ( for H being GroupWithOperators of O st H = . i holds
H is trivial ) ) )

assume A3: len s1 > len s2 ; :: thesis: ex i being Nat st
( i in dom & ( for H being GroupWithOperators of O st H = . 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 ;
then A7: i + 1 <= len s1 by FINSEQ_1:1;
0 + 1 <= i + 1 by XREAL_1:6;
then A8: 1 <= len s1 by ;
per cases ( len s1 <= 1 or len s1 > 1 ) ;
suppose len s1 <= 1 ; :: thesis: ex i being Nat st
( i in dom & ( for H being GroupWithOperators of O st H = . i holds
H is trivial ) )

then A9: len s1 = 1 by ;
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
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 ;
then A10: i = 1 by ;
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 ;
hence contradiction by FINSEQ_1:2, TARSKI:def 1; :: thesis: verum
end;
then s1 is strictly_decreasing ;
hence ex i being Nat st
( i in dom & ( for H being GroupWithOperators of O st H = . i holds
H is trivial ) ) by A1, A2, A3; :: thesis: verum
end;
suppose A12: len s1 > 1 ; :: thesis: ex i being Nat st
( i in dom & ( for H being GroupWithOperators of O st H = . i holds
H is trivial ) )

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

A13: (i + 1) - 1 <= (len s1) - 1 by ;
i in Seg (len s1) by ;
then A14: 1 <= i by FINSEQ_1:1;
len s1 = () + 1 by ;
then i in Seg () by ;
hence A15: i in dom by FINSEQ_1:def 3; :: thesis: for H being GroupWithOperators of O st H = . i holds
H is trivial

let H be GroupWithOperators of O; :: thesis: ( H = . i implies H is trivial )
assume H = . i ; :: thesis: H is trivial
hence H is trivial by ; :: thesis: verum
end;
end;