let O be set ; :: thesis:
let G be GroupWithOperators of O; :: thesis:
let s1, s2 be CompositionSeries of G; :: thesis:
assume len s1 > 1 ; :: thesis:
then len s1 >= 1 + 1 by NAT_1:13;
then Seg 2 c= Seg (len s1) by FINSEQ_1:5;
then A1: Seg 2 c= dom s1 by FINSEQ_1:def 3;
assume A2: s2 <> s1 ; :: thesis:
assume A3: s2 is strictly_decreasing ; :: thesis:
assume A4: s2 is_finer_than s1 ; :: thesis:
then consider n being Nat such that
A5: len s2 = (len s1) + n by Th95;
n <> 0 by A2, A4, A5, Th96;
then A6: 0 + (len s1) < n + (len s1) by XREAL_1:6;
then Seg (len s1) c= Seg (len s2) by A5, FINSEQ_1:5;
then Seg (len s1) c= dom s2 by FINSEQ_1:def 3;
then A7: dom s1 c= dom s2 by FINSEQ_1:def 3;

set fX = { k where k is Element of NAT : ( k in dom s1 & s1 . k = s2 . k ) } ;
A8: 1 in Seg 2 ;
( s1 . 1 = (Omega). G & s2 . 1 = (Omega). G ) by Def28;
then A9: 1 in { k where k is Element of NAT : ( k in dom s1 & s1 . k = s2 . k ) } by A1, A8;

let x be object ; :: thesis:
assume x in { k where k is Element of NAT : ( k in dom s1 & s1 . k = s2 . k ) } ; :: thesis:
then ex k being Element of NAT st
( x = k & k in dom s1 & s1 . k = s2 . k ) ;
hence x in dom s1 ; :: thesis:

end;

then { k where k is Element of NAT : ( k in dom s1 & s1 . k = s2 . k ) } c= dom s1 ;
then reconsider fX = { k where k is Element of NAT : ( k in dom s1 & s1 . k = s2 . k ) } as non empty finite real-membered set by A9;
set i = max fX;
max fX in fX by XXREAL_2:def 8;
then A10: ex k being Element of NAT st
( max fX = k & k in dom s1 & s1 . k = s2 . k ) ;
then reconsider i = max fX as Element of NAT ;
take i = i; :: thesis:
thus ( i in dom s1 & s1 . i = s2 . i ) by A10; :: thesis:

A11: now :: thesis:

assume not i + 1 in dom s1 ; :: thesis:
then A12: not i + 1 in Seg (len s1) by FINSEQ_1:def 3;

per cases by A12;

suppose 1 > i + 1 ; :: thesis:

then 1 - 1 > (i + 1) - 1 by XREAL_1:9;
then 0 > i ;
hence contradiction ; :: thesis:

end;

suppose A13: i + 1 > len s1 ; :: thesis:

i in Seg (len s1) by A10, FINSEQ_1:def 3;
then A14: i <= len s1 by FINSEQ_1:1;
i >= len s1 by A13, NAT_1:13;
then A15: i = len s1 by A14, XXREAL_0:1;
then ( 0 + 1 <= i + 1 & i + 1 <= len s2 ) by A5, A6, NAT_1:13;
then i + 1 in Seg (len s2) ;
then A16: i + 1 in dom s2 by FINSEQ_1:def 3;
then reconsider H1 = s2 . i, H2 = s2 . (i + 1) as Element of the_stable_subgroups_of G by A10, FINSEQ_2:11;
reconsider H1 = H1, H2 = H2 as StableSubgroup of G by Def11;
A17: s2 . i = (1). G by A10, A15, Def28;
then A18: the carrier of H1 = {(1_ G)} by Def8;
reconsider H2 = H2 as normal StableSubgroup of H1 by A7, A10, A16, Def28;
1_ G in H2 by Lm17;
then 1_ G in the carrier of H2 by STRUCT_0:def 5;
then A19: {(1_ G)} c= the carrier of H2 by ZFMISC_1:31;
H2 is Subgroup of (1). G by A17, Def7;
then the carrier of H2 c= the carrier of ((1). G) by GROUP_2:def 5;
then the carrier of H2 c= {(1_ G)} by Def8;
then the carrier of H2 = {(1_ G)} by A19, XBOOLE_0:def 10;
then H1 ./. H2 is trivial by A18, Th77;
hence contradiction by A3, A7, A10, A16; :: thesis:

end;

end;

end;

hence i + 1 in dom s1 ; :: thesis:

A20: 1 + i > 0 + i by XREAL_1:6;
assume s1 . (i + 1) = s2 . (i + 1) ; :: thesis:
then consider k being Element of NAT such that
A21: k > i and
A22: ( k in dom s1 & s1 . k = s2 . k ) by A11, A20;
k in fX by A22;
hence contradiction by A21, XXREAL_2:def 8; :: thesis:

end;

hence s1 . (i + 1) <> s2 . (i + 1) ; :: thesis:

end;

then consider i being Nat such that
A23: i in dom s1 and
A24: i + 1 in dom s1 and
A25: s1 . i = s2 . i and
A26: s1 . (i + 1) <> s2 . (i + 1) ;

consider x being set such that
A27: x c= dom s2 and
A28: s1 = s2 * (Sgm x) by A4;
set j = (Sgm x) . (i + 1);
A29: x c= Seg (len s2) by A27, FINSEQ_1:def 3;
then a29: x is included_in_Seg ;
A30: i + 1 in dom (Sgm x) by A24, A28, FUNCT_1:11;
then (Sgm x) . (i + 1) in rng (Sgm x) by FUNCT_1:3;
then (Sgm x) . (i + 1) in x by a29, FINSEQ_1:def 14;
then A31: (Sgm x) . (i + 1) in Seg (len s2) by A29;
then reconsider j = (Sgm x) . (i + 1) as Element of NAT ;
A32: i + 1 <= j by a29, A30, FINSEQ_3:152;
take j = j; :: thesis:
thus j in dom s2 by A31, FINSEQ_1:def 3; :: thesis:
thus s1 . (i + 1) = s2 . j by A24, A28, FUNCT_1:12; :: thesis:
j <> i + 1 by A24, A26, A28, FUNCT_1:12;
hence i + 1 < j by A32, XXREAL_0:1; :: thesis:

end;

then consider j being Nat such that
A33: ( j in dom s2 & i + 1 < j ) and
A34: s1 . (i + 1) = s2 . j ;
take i ; :: thesis:
take j ; :: thesis:
thus ( i in dom s1 & i in dom s2 ) by A7, A23; :: thesis:
thus ( i + 1 in dom s1 & i + 1 in dom s2 ) by A7, A24; :: thesis:
thus ( j in dom s2 & i + 1 < j ) by A33; :: thesis:
thus ( s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) ) by A25, A26; :: thesis:
thus s1 . (i + 1) = s2 . j by A34; :: thesis: