let O be set ; :: thesis:
let G be GroupWithOperators of O; :: thesis:
let s1, s2 be CompositionSeries of G; :: thesis:
assume A1: s1 is_finer_than s2 ; :: thesis:
assume A2: s2 is jordan_holder ; :: thesis:
assume A3: len s1 > len s2 ; :: thesis:
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 ;

suppose len s1 <= 1 ; :: thesis:

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

now :: thesis:

let i be Nat; :: thesis:
assume i in dom s1 ; :: thesis:
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:
let H1 be StableSubgroup of G; :: thesis:
let N1 be normal StableSubgroup of H1; :: thesis:
assume H1 = s1 . i ; :: thesis:
assume N1 = s1 . (i + 1) ; :: thesis:
assume H1 ./. N1 is trivial ; :: thesis:
2 in Seg 1 by A9, A10, A11, FINSEQ_1:def 3;
hence contradiction by FINSEQ_1:2, TARSKI:def 1; :: thesis:

end;

then s1 is strictly_decreasing ;
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:

end;

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

take i ; :: thesis:
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:
let H be GroupWithOperators of O; :: thesis:
assume H = (the_series_of_quotients_of s1) . i ; :: thesis:
hence H is trivial by A6, A12, A15, Def33; :: thesis:

end;

end;