let O be set ; :: thesis: for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st len s1 > 1 & s2 <> s1 & s2 is strictly_decreasing & s2 is_finer_than s1 holds
ex i, j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )

let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G st len s1 > 1 & s2 <> s1 & s2 is strictly_decreasing & s2 is_finer_than s1 holds
ex i, j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )

let s1, s2 be CompositionSeries of G; :: thesis: ( len s1 > 1 & s2 <> s1 & s2 is strictly_decreasing & s2 is_finer_than s1 implies ex i, j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j ) )

assume len s1 > 1 ; :: thesis: ( not s2 <> s1 or not s2 is strictly_decreasing or not s2 is_finer_than s1 or ex i, j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j ) )

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: ( not s2 is strictly_decreasing or not s2 is_finer_than s1 or ex i, j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j ) )

assume A3: s2 is strictly_decreasing ; :: thesis: ( not s2 is_finer_than s1 or ex i, j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j ) )

assume A4: s2 is_finer_than s1 ; :: thesis: ex i, j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )

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 ;
then Seg (len s1) c= dom s2 by FINSEQ_1:def 3;
then A7: dom s1 c= dom s2 by FINSEQ_1:def 3;
now :: thesis: ex i being Element of NAT st
( i in dom s1 & s1 . i = s2 . i & i + 1 in dom s1 & s1 . (i + 1) <> s2 . (i + 1) )
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;
now :: thesis: for x being object st x in { k where k is Element of NAT : ( k in dom s1 & s1 . k = s2 . k ) } holds
x in dom s1
let x be object ; :: thesis: ( x in { k where k is Element of NAT : ( k in dom s1 & s1 . k = s2 . k ) } implies x in dom s1 )
assume x in { k where k is Element of NAT : ( k in dom s1 & s1 . k = s2 . k ) } ; :: thesis: x in dom s1
then ex k being Element of NAT st
( x = k & k in dom s1 & s1 . k = s2 . k ) ;
hence x in dom s1 ; :: thesis: verum
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: ( i in dom s1 & s1 . i = s2 . i & i + 1 in dom s1 & s1 . (i + 1) <> s2 . (i + 1) )
thus ( i in dom s1 & s1 . i = s2 . i ) by A10; :: thesis: ( i + 1 in dom s1 & s1 . (i + 1) <> s2 . (i + 1) )
A11: now :: thesis: i + 1 in dom s1
assume not i + 1 in dom s1 ; :: thesis: contradiction
then A12: not i + 1 in Seg (len s1) by FINSEQ_1:def 3;
per cases ( 1 > i + 1 or i + 1 > len s1 ) by A12;
suppose 1 > i + 1 ; :: thesis: contradiction
end;
suppose A13: i + 1 > len s1 ; :: thesis: contradiction
i in Seg (len s1) by ;
then A14: i <= len s1 by FINSEQ_1:1;
i >= len s1 by ;
then A15: i = len s1 by ;
then ( 0 + 1 <= i + 1 & i + 1 <= len s2 ) by ;
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 ;
reconsider H1 = H1, H2 = H2 as StableSubgroup of G by Def11;
A17: s2 . i = (1). G by ;
then A18: the carrier of H1 = {(1_ G)} by Def8;
reconsider H2 = H2 as normal StableSubgroup of H1 by ;
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 ;
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 ;
then H1 ./. H2 is trivial by ;
hence contradiction by A3, A7, A10, A16; :: thesis: verum
end;
end;
end;
hence i + 1 in dom s1 ; :: thesis: s1 . (i + 1) <> s2 . (i + 1)
now :: thesis: not s1 . (i + 1) = s2 . (i + 1)
A20: 1 + i > 0 + i by XREAL_1:6;
assume s1 . (i + 1) = s2 . (i + 1) ; :: thesis: contradiction
then consider k being Element of NAT such that
A21: k > i and
A22: ( k in dom s1 & s1 . k = s2 . k ) by ;
k in fX by A22;
hence contradiction by A21, XXREAL_2:def 8; :: thesis: verum
end;
hence s1 . (i + 1) <> s2 . (i + 1) ; :: thesis: verum
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) ;
now :: thesis: ex j being Element of NAT st
( j in dom s2 & s1 . (i + 1) = s2 . j & i + 1 < j )
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 ;
A30: i + 1 in dom (Sgm x) by ;
then (Sgm x) . (i + 1) in rng (Sgm x) by FUNCT_1:3;
then (Sgm x) . (i + 1) in x by ;
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 ;
take j = j; :: thesis: ( j in dom s2 & s1 . (i + 1) = s2 . j & i + 1 < j )
thus j in dom s2 by ; :: thesis: ( s1 . (i + 1) = s2 . j & i + 1 < j )
thus s1 . (i + 1) = s2 . j by ; :: thesis: i + 1 < j
j <> i + 1 by ;
hence i + 1 < j by ; :: thesis: verum
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: ex j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )

take j ; :: thesis: ( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )
thus ( i in dom s1 & i in dom s2 ) by ; :: thesis: ( i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )
thus ( i + 1 in dom s1 & i + 1 in dom s2 ) by ; :: thesis: ( j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )
thus ( j in dom s2 & i + 1 < j ) by A33; :: thesis: ( s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )
thus ( s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) ) by ; :: thesis: s1 . (i + 1) = s2 . j
thus s1 . (i + 1) = s2 . j by A34; :: thesis: verum