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 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;

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) ;

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 A7, A23; :: 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 A7, A24; :: 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 A25, A26; :: thesis: s1 . (i + 1) = s2 . j

thus s1 . (i + 1) = s2 . j by A34; :: thesis: verum

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 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;

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) )

then consider i being Nat such that ( 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;

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) )

end;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

then
{ k where k is Element of NAT : ( k in dom s1 & s1 . k = s2 . k ) } c= dom s1
;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;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

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

hence
i + 1 in dom s1
; :: thesis: s1 . (i + 1) <> s2 . (i + 1)assume
not i + 1 in dom s1
; :: thesis: contradiction

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

end;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;

end;

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

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: verum

end;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: verum

now :: thesis: not s1 . (i + 1) = s2 . (i + 1)

hence
s1 . (i + 1) <> s2 . (i + 1)
; :: thesis: verumA20:
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 A11, A20;

k in fX by A22;

hence contradiction by A21, XXREAL_2:def 8; :: thesis: verum

end;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 A11, A20;

k in fX by A22;

hence contradiction by A21, XXREAL_2:def 8; :: thesis: verum

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 )

then consider j being Nat such that ( 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 A27, FINSEQ_1:def 3;

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 13;

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: ( j in dom s2 & s1 . (i + 1) = s2 . j & i + 1 < j )

thus j in dom s2 by A31, FINSEQ_1:def 3; :: thesis: ( s1 . (i + 1) = s2 . j & i + 1 < j )

thus s1 . (i + 1) = s2 . j by A24, A28, FUNCT_1:12; :: thesis: i + 1 < j

j <> i + 1 by A24, A26, A28, FUNCT_1:12;

hence i + 1 < j by A32, XXREAL_0:1; :: thesis: verum

end;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;

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 13;

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: ( j in dom s2 & s1 . (i + 1) = s2 . j & i + 1 < j )

thus j in dom s2 by A31, FINSEQ_1:def 3; :: thesis: ( s1 . (i + 1) = s2 . j & i + 1 < j )

thus s1 . (i + 1) = s2 . j by A24, A28, FUNCT_1:12; :: thesis: i + 1 < j

j <> i + 1 by A24, A26, A28, FUNCT_1:12;

hence i + 1 < j by A32, XXREAL_0:1; :: thesis: verum

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 A7, A23; :: 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 A7, A24; :: 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 A25, A26; :: thesis: s1 . (i + 1) = s2 . j

thus s1 . (i + 1) = s2 . j by A34; :: thesis: verum