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 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 holds
y is strict GroupWithOperators of O

let y be set ; :: thesis: for s1 being CompositionSeries of G st y in rng holds
y is strict GroupWithOperators of O

let s1 be CompositionSeries of G; :: thesis: ( y in rng implies y is strict GroupWithOperators of O )
assume A1: y in rng ; :: thesis: y is strict GroupWithOperators of O
set f1 = the_series_of_quotients_of s1;
A2: ( len = 0 or len >= 0 + 1 ) by NAT_1:13;
per cases by A2;
suppose len = 0 ; :: thesis: y is strict GroupWithOperators of O
end;
suppose len >= 1 ; :: thesis: y is strict GroupWithOperators of O
then A3: len s1 > 1 by ;
then A4: len s1 = () + 1 by Def33;
consider i being object such that
A5: i in dom and
A6: (the_series_of_quotients_of s1) . i = y by ;
reconsider i = i as Nat by A5;
A7: i in Seg () by ;
then A8: 1 <= i by FINSEQ_1:1;
1 <= i by ;
then 1 + 1 <= i + 1 by XREAL_1:6;
then A9: 1 <= i + 1 by XXREAL_0:2;
A10: i <= len by ;
then ( 0 + i <= 1 + i & i + 1 <= () + 1 ) by XREAL_1:6;
then i <= len s1 by ;
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 <= () + 1 by ;
then i + 1 <= len s1 by ;
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 ;
y = H1 ./. N1 by A3, A5, A6, Def33;
hence y is strict GroupWithOperators of O ; :: thesis: verum
end;
end;