let O be set ; :: thesis:
let G be GroupWithOperators of O; :: thesis:
let s1 be CompositionSeries of G; :: thesis:
let i be Nat; :: thesis:
assume A1: i in dom (the_series_of_quotients_of s1) ; :: thesis:
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:
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 by A3, XXREAL_0:1;

suppose len (the_series_of_quotients_of s1) = 0 ; :: thesis:

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:

end;

suppose A4: len (the_series_of_quotients_of s1) = 1 ; :: thesis:

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

end;

suppose A13: len (the_series_of_quotients_of s1) > 1 ; :: thesis:

(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 <= (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:
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:

end;

end;