let O be set ; 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; 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 ; 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; ( 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)
; 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) >= 1
;
y is strict GroupWithOperators of Othen 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
;
verum end; end;