let O be set ; :: thesis: for G being GroupWithOperators of O

for s1 being CompositionSeries of G

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

( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) )

let G be GroupWithOperators of O; :: thesis: for s1 being CompositionSeries of G

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

( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) )

let s1 be CompositionSeries of G; :: thesis: for 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 ) holds

( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) )

let i be Nat; :: thesis: ( 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 ) implies ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) ) )

assume A1: i in dom (the_series_of_quotients_of s1) ; :: thesis: ( ex H being GroupWithOperators of O st

( H = (the_series_of_quotients_of s1) . i & not H is trivial ) or ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) ) )

set f1 = the_series_of_quotients_of s1;

assume A2: for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ; :: thesis: ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) )

A3: ( len (the_series_of_quotients_of s1) = 0 or len (the_series_of_quotients_of s1) >= 0 + 1 ) by NAT_1:13;

for s1 being CompositionSeries of G

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

( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) )

let G be GroupWithOperators of O; :: thesis: for s1 being CompositionSeries of G

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

( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) )

let s1 be CompositionSeries of G; :: thesis: for 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 ) holds

( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) )

let i be Nat; :: thesis: ( 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 ) implies ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) ) )

assume A1: i in dom (the_series_of_quotients_of s1) ; :: thesis: ( ex H being GroupWithOperators of O st

( H = (the_series_of_quotients_of s1) . i & not H is trivial ) or ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) ) )

set f1 = the_series_of_quotients_of s1;

assume A2: for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds

H is trivial ; :: thesis: ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) )

A3: ( len (the_series_of_quotients_of s1) = 0 or len (the_series_of_quotients_of s1) >= 0 + 1 ) by NAT_1:13;

per cases
( len (the_series_of_quotients_of s1) = 0 or len (the_series_of_quotients_of s1) = 1 or len (the_series_of_quotients_of s1) > 1 )
by A3, XXREAL_0:1;

end;

suppose
len (the_series_of_quotients_of s1) = 0
; :: thesis: ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) )

then
the_series_of_quotients_of s1 = {}
;

hence ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) ) by A1; :: thesis: verum

end;hence ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) ) by A1; :: thesis: verum

suppose A4:
len (the_series_of_quotients_of s1) = 1
; :: thesis: ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) )

(the_series_of_quotients_of s1) . i in rng (the_series_of_quotients_of s1)
by A1, FUNCT_1:3;

then reconsider H = (the_series_of_quotients_of s1) . i as strict GroupWithOperators of O by Th102;

set H1 = (Omega). G;

A5: H is trivial by A2;

A6: len s1 > 1 by A4, Def33, CARD_1:27;

then A7: len s1 = (len (the_series_of_quotients_of s1)) + 1 by Def33;

then A8: s1 . 2 = (1). G by A4, Def28;

i in Seg 1 by A1, A4, FINSEQ_1:def 3;

then A9: i = 1 by FINSEQ_1:2, TARSKI:def 1;

then i in Seg 2 ;

hence i in dom s1 by A4, A7, FINSEQ_1:def 3; :: thesis: ( i + 1 in dom s1 & s1 . i = s1 . (i + 1) )

reconsider N1 = (1). G as StableSubgroup of (Omega). G by Th16;

A10: s1 . 1 = (Omega). G by Def28;

A11: (1). G = (1). ((Omega). G) by Th15;

then reconsider N1 = N1 as normal StableSubgroup of (Omega). G ;

A12: (Omega). G,((Omega). G) ./. N1 are_isomorphic by A11, Th56;

i + 1 in Seg 2 by A9;

hence i + 1 in dom s1 by A4, A7, FINSEQ_1:def 3; :: thesis: s1 . i = s1 . (i + 1)

for H1 being StableSubgroup of G

for N1 being normal StableSubgroup of H1 st H1 = s1 . i & N1 = s1 . (i + 1) holds

(the_series_of_quotients_of s1) . i = H1 ./. N1 by A1, A6, Def33;

then ((Omega). G) ./. N1 is trivial by A10, A8, A9, A5;

hence s1 . i = s1 . (i + 1) by A10, A8, A9, A11, A12, Th42, Th58; :: thesis: verum

end;then reconsider H = (the_series_of_quotients_of s1) . i as strict GroupWithOperators of O by Th102;

set H1 = (Omega). G;

A5: H is trivial by A2;

A6: len s1 > 1 by A4, Def33, CARD_1:27;

then A7: len s1 = (len (the_series_of_quotients_of s1)) + 1 by Def33;

then A8: s1 . 2 = (1). G by A4, Def28;

i in Seg 1 by A1, A4, FINSEQ_1:def 3;

then A9: i = 1 by FINSEQ_1:2, TARSKI:def 1;

then i in Seg 2 ;

hence i in dom s1 by A4, A7, FINSEQ_1:def 3; :: thesis: ( i + 1 in dom s1 & s1 . i = s1 . (i + 1) )

reconsider N1 = (1). G as StableSubgroup of (Omega). G by Th16;

A10: s1 . 1 = (Omega). G by Def28;

A11: (1). G = (1). ((Omega). G) by Th15;

then reconsider N1 = N1 as normal StableSubgroup of (Omega). G ;

A12: (Omega). G,((Omega). G) ./. N1 are_isomorphic by A11, Th56;

i + 1 in Seg 2 by A9;

hence i + 1 in dom s1 by A4, A7, FINSEQ_1:def 3; :: thesis: s1 . i = s1 . (i + 1)

for H1 being StableSubgroup of G

for N1 being normal StableSubgroup of H1 st H1 = s1 . i & N1 = s1 . (i + 1) holds

(the_series_of_quotients_of s1) . i = H1 ./. N1 by A1, A6, Def33;

then ((Omega). G) ./. N1 is trivial by A10, A8, A9, A5;

hence s1 . i = s1 . (i + 1) by A10, A8, A9, A11, A12, Th42, Th58; :: thesis: verum

suppose A13:
len (the_series_of_quotients_of s1) > 1
; :: thesis: ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) )

(the_series_of_quotients_of s1) . i in rng (the_series_of_quotients_of s1)
by A1, FUNCT_1:3;

then reconsider H = (the_series_of_quotients_of s1) . i as strict GroupWithOperators of O by Th102;

A14: i in Seg (len (the_series_of_quotients_of s1)) by A1, FINSEQ_1:def 3;

then A15: 1 <= i by FINSEQ_1:1;

1 <= i by A14, FINSEQ_1:1;

then 1 + 1 <= i + 1 by XREAL_1:6;

then A16: 1 <= i + 1 by XXREAL_0:2;

A17: i <= len (the_series_of_quotients_of s1) by A14, FINSEQ_1:1;

then A18: ( 0 + i <= 1 + i & i + 1 <= (len (the_series_of_quotients_of s1)) + 1 ) by XREAL_1:6;

A19: len s1 > 1 by A13, Def33, CARD_1:27;

then len s1 = (len (the_series_of_quotients_of s1)) + 1 by Def33;

then i <= len s1 by A18, XXREAL_0:2;

then A20: i in Seg (len s1) by A15;

hence i in dom s1 by FINSEQ_1:def 3; :: thesis: ( i + 1 in dom s1 & s1 . i = s1 . (i + 1) )

i + 1 <= (len (the_series_of_quotients_of s1)) + 1 by A17, XREAL_1:6;

then i + 1 <= len s1 by A19, Def33;

then A21: i + 1 in Seg (len s1) by A16;

hence i + 1 in dom s1 by FINSEQ_1:def 3; :: thesis: s1 . i = s1 . (i + 1)

A22: i + 1 in dom s1 by A21, FINSEQ_1:def 3;

then s1 . (i + 1) in the_stable_subgroups_of G by FINSEQ_2:11;

then reconsider N1 = s1 . (i + 1) as strict StableSubgroup of G by Def11;

A23: i in dom s1 by A20, FINSEQ_1:def 3;

then s1 . i in the_stable_subgroups_of G by FINSEQ_2:11;

then reconsider H1 = s1 . i as strict StableSubgroup of G by Def11;

reconsider N1 = N1 as normal StableSubgroup of H1 by A23, A22, Def28;

H is trivial by A2;

then H1 ./. N1 is trivial by A1, A19, Def33;

hence s1 . i = s1 . (i + 1) by Th76; :: thesis: verum

end;then reconsider H = (the_series_of_quotients_of s1) . i as strict GroupWithOperators of O by Th102;

A14: i in Seg (len (the_series_of_quotients_of s1)) by A1, FINSEQ_1:def 3;

then A15: 1 <= i by FINSEQ_1:1;

1 <= i by A14, FINSEQ_1:1;

then 1 + 1 <= i + 1 by XREAL_1:6;

then A16: 1 <= i + 1 by XXREAL_0:2;

A17: i <= len (the_series_of_quotients_of s1) by A14, FINSEQ_1:1;

then A18: ( 0 + i <= 1 + i & i + 1 <= (len (the_series_of_quotients_of s1)) + 1 ) by XREAL_1:6;

A19: len s1 > 1 by A13, Def33, CARD_1:27;

then len s1 = (len (the_series_of_quotients_of s1)) + 1 by Def33;

then i <= len s1 by A18, XXREAL_0:2;

then A20: i in Seg (len s1) by A15;

hence i in dom s1 by FINSEQ_1:def 3; :: thesis: ( i + 1 in dom s1 & s1 . i = s1 . (i + 1) )

i + 1 <= (len (the_series_of_quotients_of s1)) + 1 by A17, XREAL_1:6;

then i + 1 <= len s1 by A19, Def33;

then A21: i + 1 in Seg (len s1) by A16;

hence i + 1 in dom s1 by FINSEQ_1:def 3; :: thesis: s1 . i = s1 . (i + 1)

A22: i + 1 in dom s1 by A21, FINSEQ_1:def 3;

then s1 . (i + 1) in the_stable_subgroups_of G by FINSEQ_2:11;

then reconsider N1 = s1 . (i + 1) as strict StableSubgroup of G by Def11;

A23: i in dom s1 by A20, FINSEQ_1:def 3;

then s1 . i in the_stable_subgroups_of G by FINSEQ_2:11;

then reconsider H1 = s1 . i as strict StableSubgroup of G by Def11;

reconsider N1 = N1 as normal StableSubgroup of H1 by A23, A22, Def28;

H is trivial by A2;

then H1 ./. N1 is trivial by A1, A19, Def33;

hence s1 . i = s1 . (i + 1) by Th76; :: thesis: verum