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 & ( for H being GroupWithOperators of O st H = . 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 & ( for H being GroupWithOperators of O st H = . 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 & ( for H being GroupWithOperators of O st H = . 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 & ( for H being GroupWithOperators of O st H = . 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 ; :: thesis: ( ex H being GroupWithOperators of O st
( H = . 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 = . i holds
H is trivial ; :: thesis: ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) )
A3: ( len = 0 or len >= 0 + 1 ) by NAT_1:13;
per cases ( len = 0 or len = 1 or len > 1 ) by ;
suppose len = 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;
suppose A4: len = 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 by ;
then reconsider H = . i as strict GroupWithOperators of O by Th102;
set H1 = (Omega). G;
A5: H is trivial by A2;
A6: len s1 > 1 by ;
then A7: len s1 = () + 1 by Def33;
then A8: s1 . 2 = (1). G by ;
i in Seg 1 by ;
then A9: i = 1 by ;
then i in Seg 2 ;
hence i in dom s1 by ; :: 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). () by Th15;
then reconsider N1 = N1 as normal StableSubgroup of (Omega). G ;
A12: (Omega). G,() ./. N1 are_isomorphic by ;
i + 1 in Seg 2 by A9;
hence i + 1 in dom s1 by ; :: 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
. i = H1 ./. N1 by ;
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;
suppose A13: len > 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 by ;
then reconsider H = . i as strict GroupWithOperators of O by Th102;
A14: i in Seg () by ;
then A15: 1 <= i by FINSEQ_1:1;
1 <= i by ;
then 1 + 1 <= i + 1 by XREAL_1:6;
then A16: 1 <= i + 1 by XXREAL_0:2;
A17: i <= len by ;
then A18: ( 0 + i <= 1 + i & i + 1 <= () + 1 ) by XREAL_1:6;
A19: len s1 > 1 by ;
then len s1 = () + 1 by Def33;
then i <= len s1 by ;
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 <= () + 1 by ;
then i + 1 <= len s1 by ;
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 ;
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 ;
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 ;
H is trivial by A2;
then H1 ./. N1 is trivial by ;
hence s1 . i = s1 . (i + 1) by Th76; :: thesis: verum
end;
end;