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;

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;

end;

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;hence y is strict GroupWithOperators of O by A1; :: thesis: verum

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;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