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 A3:
len (the_series_of_quotients_of s1) >= 1
;
:: thesis: y is strict GroupWithOperators of OA4:
len s1 > 1
by A3, Def36, CARD_1:47;
then A5:
len s1 = (len (the_series_of_quotients_of s1)) + 1
by Def36;
consider i being
set such that A6:
(
i in dom (the_series_of_quotients_of s1) &
(the_series_of_quotients_of s1) . i = y )
by A1, FUNCT_1:def 5;
reconsider i =
i as
Nat by A6;
A7:
0 + i <= 1
+ i
by XREAL_1:8;
i in Seg (len (the_series_of_quotients_of s1))
by A6, FINSEQ_1:def 3;
then A8:
( 1
<= i &
i <= len (the_series_of_quotients_of s1) )
by FINSEQ_1:3;
then
( 1
<= i &
i + 1
<= (len (the_series_of_quotients_of s1)) + 1 )
by XREAL_1:8;
then
( 1
<= i &
i <= len s1 )
by A5, A7, XXREAL_0:2;
then
i in Seg (len s1)
by FINSEQ_1:3;
then A9:
i in dom s1
by FINSEQ_1:def 3;
then
s1 . i in the_stable_subgroups_of G
by FINSEQ_2:13;
then reconsider H1 =
s1 . i as
strict StableSubgroup of
G by Def11;
( 1
+ 1
<= i + 1 &
i + 1
<= (len (the_series_of_quotients_of s1)) + 1 )
by A8, XREAL_1:8;
then
( 1
<= i + 1 &
i + 1
<= len s1 )
by A4, Def36, XXREAL_0:2;
then
i + 1
in Seg (len s1)
;
then A10:
i + 1
in dom s1
by FINSEQ_1:def 3;
then
s1 . (i + 1) in the_stable_subgroups_of G
by FINSEQ_2:13;
then reconsider N1 =
s1 . (i + 1) as
strict StableSubgroup of
G by Def11;
reconsider N1 =
N1 as
normal StableSubgroup of
H1 by A9, A10, Def31;
y = H1 ./. N1
by A4, A6, Def36;
hence
y is
strict GroupWithOperators of
O
;
:: thesis: verum end;