let O be set ; :: thesis: for G being GroupWithOperators of O
for y being set
for s1 being CompositionSeries of G st y in rng (the_series_of_quotients_of s1) holds
y is strict GroupWithOperators of O
let G be GroupWithOperators of O; :: thesis: for y being set
for s1 being CompositionSeries of G st y in rng (the_series_of_quotients_of s1) holds
y is strict GroupWithOperators of O
let y be set ; :: thesis: for s1 being CompositionSeries of G st y in rng (the_series_of_quotients_of s1) holds
y is strict GroupWithOperators of O
let s1 be CompositionSeries of G; :: thesis: ( y in rng (the_series_of_quotients_of s1) implies y is strict GroupWithOperators of O )
assume A1: y in rng (the_series_of_quotients_of s1) ; :: thesis: y is strict GroupWithOperators of O
set f1 = the_series_of_quotients_of s1;
A2: ( 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 ) by A2;

suppose len (the_series_of_quotients_of s1) = 0 ; :: thesis: y is strict GroupWithOperators of O

then the_series_of_quotients_of s1 = {} ;
hence y is strict GroupWithOperators of O by A1; :: thesis: verum

end;

suppose len (the_series_of_quotients_of s1) >= 1 ; :: thesis: y is strict GroupWithOperators of O

then A3: len s1 > 1 by Def33, CARD_1:27;
then A4: len s1 = (len (the_series_of_quotients_of s1)) + 1 by Def33;
consider i being object such that
A5: i in dom (the_series_of_quotients_of s1) and
A6: (the_series_of_quotients_of s1) . i = y by A1, FUNCT_1:def 3;
reconsider i = i as Nat by A5;
A7: i in Seg (len (the_series_of_quotients_of s1)) by A5, FINSEQ_1:def 3;
then A8: 1 <= i by FINSEQ_1:1;
1 <= i by A7, FINSEQ_1:1;
then 1 + 1 <= i + 1 by XREAL_1:6;
then A9: 1 <= i + 1 by XXREAL_0:2;
A10: i <= len (the_series_of_quotients_of s1) by A7, FINSEQ_1:1;
then ( 0 + i <= 1 + i & i + 1 <= (len (the_series_of_quotients_of s1)) + 1 ) by XREAL_1:6;
then i <= len s1 by A4, XXREAL_0:2;
then i in Seg (len s1) by A8;
then A11: i in dom s1 by 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;
i + 1 <= (len (the_series_of_quotients_of s1)) + 1 by A10, XREAL_1:6;
then i + 1 <= len s1 by A3, Def33;
then i + 1 in Seg (len s1) by A9;
then A12: i + 1 in dom s1 by 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;
reconsider N1 = N1 as normal StableSubgroup of H1 by A11, A12, Def28;
y = H1 ./. N1 by A3, A5, A6, Def33;
hence y is strict GroupWithOperators of O ; :: thesis: verum

end;

end;