let O be set ; for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G
for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s2 = Del s1,i holds
the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i
let G be GroupWithOperators of O; for s1, s2 being CompositionSeries of G
for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s2 = Del s1,i holds
the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i
let s1, s2 be CompositionSeries of G; for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s2 = Del s1,i holds
the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i
let i be Nat; ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s2 = Del s1,i implies the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i )
set f1 = the_series_of_quotients_of s1;
assume A1:
i in dom s1
; ( not i + 1 in dom s1 or not s1 . i = s1 . (i + 1) or not s2 = Del s1,i or the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i )
then consider k being Nat such that
A2:
len s1 = k + 1
and
A3:
len (Del s1,i) = k
by FINSEQ_3:113;
assume
i + 1 in dom s1
; ( not s1 . i = s1 . (i + 1) or not s2 = Del s1,i or the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i )
then
i + 1 in Seg (len s1)
by FINSEQ_1:def 3;
then A4:
i + 1 <= len s1
by FINSEQ_1:3;
assume A5:
s1 . i = s1 . (i + 1)
; ( not s2 = Del s1,i or the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i )
A6:
i in Seg (len s1)
by A1, FINSEQ_1:def 3;
then
1 <= i
by FINSEQ_1:3;
then A7:
1 + 1 <= i + 1
by XREAL_1:8;
then
2 <= len s1
by A4, XXREAL_0:2;
then A8:
1 < len s1
by XXREAL_0:2;
then A9:
len s1 = (len (the_series_of_quotients_of s1)) + 1
by Def36;
assume A10:
s2 = Del s1,i
; the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i
then
1 + 1 <= (len s2) + 1
by A7, A4, A2, A3, XXREAL_0:2;
then A11:
1 <= len s2
by XREAL_1:8;
per cases
( len s2 = 1 or len s2 > 1 )
by A11, XXREAL_0:1;
suppose A12:
len s2 = 1
;
the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),ithen
1
in Seg (len (the_series_of_quotients_of s1))
by A10, A2, A3, A9;
then
1
in dom (the_series_of_quotients_of s1)
by FINSEQ_1:def 3;
then A13:
ex
k1 being
Nat st
(
len (the_series_of_quotients_of s1) = k1 + 1 &
len (Del (the_series_of_quotients_of s1),1) = k1 )
by FINSEQ_3:113;
A14:
1
<= i
by A6, FINSEQ_1:3;
A15:
the_series_of_quotients_of s2 = {}
by A12, Def36;
i <= 1
by A10, A4, A2, A3, A12, XREAL_1:8;
then
len (Del (the_series_of_quotients_of s1),i) = 0
by A10, A2, A3, A9, A12, A13, A14, XXREAL_0:1;
hence
the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),
i
by A15;
verum end; suppose A16:
len s2 > 1
;
the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i
(
(i + 1) - 1
<= (len s1) - 1 & 1
<= i )
by A6, A4, FINSEQ_1:3, XREAL_1:11;
then
i in Seg (len (the_series_of_quotients_of s1))
by A9, FINSEQ_1:3;
then A17:
i in dom (the_series_of_quotients_of s1)
by FINSEQ_1:def 3;
then consider k1 being
Nat such that A18:
len (the_series_of_quotients_of s1) = k1 + 1
and A19:
len (Del (the_series_of_quotients_of s1),i) = k1
by FINSEQ_3:113;
now let n be
Nat;
( n in dom (Del (the_series_of_quotients_of s1),i) implies for H1 being StableSubgroup of G
for N1 being normal StableSubgroup of H1 st H1 = s2 . n & N1 = s2 . (n + 1) holds
(Del (the_series_of_quotients_of s1),i) . b3 = b4 ./. b5 )set n1 =
n + 1;
assume
n in dom (Del (the_series_of_quotients_of s1),i)
;
for H1 being StableSubgroup of G
for N1 being normal StableSubgroup of H1 st H1 = s2 . n & N1 = s2 . (n + 1) holds
(Del (the_series_of_quotients_of s1),i) . b3 = b4 ./. b5then A21:
n in Seg (len (Del (the_series_of_quotients_of s1),i))
by FINSEQ_1:def 3;
then A22:
n <= k1
by A19, FINSEQ_1:3;
then A23:
n + 1
<= k
by A2, A9, A18, XREAL_1:8;
1
<= n
by A21, FINSEQ_1:3;
then
1
+ 1
<= n + 1
by XREAL_1:8;
then
1
<= n + 1
by XXREAL_0:2;
then
n + 1
in Seg (len (the_series_of_quotients_of s1))
by A2, A9, A23;
then A24:
n + 1
in dom (the_series_of_quotients_of s1)
by FINSEQ_1:def 3;
reconsider n1 =
n + 1 as
Nat ;
let H1 be
StableSubgroup of
G;
for N1 being normal StableSubgroup of H1 st H1 = s2 . n & N1 = s2 . (n + 1) holds
(Del (the_series_of_quotients_of s1),i) . b2 = b3 ./. b4let N1 be
normal StableSubgroup of
H1;
( H1 = s2 . n & N1 = s2 . (n + 1) implies (Del (the_series_of_quotients_of s1),i) . b1 = b2 ./. b3 )assume A25:
H1 = s2 . n
;
( N1 = s2 . (n + 1) implies (Del (the_series_of_quotients_of s1),i) . b1 = b2 ./. b3 )
0 + n < 1
+ n
by XREAL_1:8;
then A26:
n <= k
by A23, XXREAL_0:2;
((len (the_series_of_quotients_of s1)) - (len (Del (the_series_of_quotients_of s1),i))) + (len (Del (the_series_of_quotients_of s1),i)) > 0 + (len (Del (the_series_of_quotients_of s1),i))
by A18, A19, XREAL_1:8;
then
Seg (len (Del (the_series_of_quotients_of s1),i)) c= Seg (len (the_series_of_quotients_of s1))
by FINSEQ_1:7;
then
n in Seg (len (the_series_of_quotients_of s1))
by A21;
then A27:
n in dom (the_series_of_quotients_of s1)
by FINSEQ_1:def 3;
assume A28:
N1 = s2 . (n + 1)
;
(Del (the_series_of_quotients_of s1),i) . b1 = b2 ./. b3per cases
( n < i or n >= i )
;
suppose A29:
n < i
;
(Del (the_series_of_quotients_of s1),i) . b1 = b2 ./. b3then A30:
n1 <= i
by NAT_1:13;
per cases
( n1 < i or n1 = i )
by A30, XXREAL_0:1;
suppose A31:
n1 < i
;
(Del (the_series_of_quotients_of s1),i) . b1 = b2 ./. b3reconsider n9 =
n as
Element of
NAT by INT_1:16;
A32:
s1 . (n9 + 1) = N1
by A10, A28, A31, FINSEQ_3:119;
s1 . n9 = H1
by A10, A25, A29, FINSEQ_3:119;
then
(the_series_of_quotients_of s1) . n = H1 ./. N1
by A8, A27, A32, Def36;
hence
(Del (the_series_of_quotients_of s1),i) . n = H1 ./. N1
by A29, FINSEQ_3:119;
verum end; suppose
n1 = i
;
(Del (the_series_of_quotients_of s1),i) . b1 = b2 ./. b3then
(
s1 . n = H1 &
s1 . (n + 1) = N1 )
by A1, A5, A10, A2, A25, A28, A23, A29, FINSEQ_3:119, FINSEQ_3:120;
then
(the_series_of_quotients_of s1) . n = H1 ./. N1
by A8, A27, Def36;
hence
(Del (the_series_of_quotients_of s1),i) . n = H1 ./. N1
by A29, FINSEQ_3:119;
verum end; end; suppose A33:
n >= i
;
(Del (the_series_of_quotients_of s1),i) . b1 = b2 ./. b3reconsider n19 =
n1 as
Element of
NAT ;
(
0 + i < 1
+ i &
n + 1
>= i + 1 )
by A33, XREAL_1:8;
then
n1 >= i
by XXREAL_0:2;
then A34:
s1 . (n19 + 1) = N1
by A1, A10, A2, A28, A23, FINSEQ_3:120;
s1 . n19 = H1
by A1, A10, A2, A25, A26, A33, FINSEQ_3:120;
then
(the_series_of_quotients_of s1) . n1 = H1 ./. N1
by A8, A24, A34, Def36;
hence
(Del (the_series_of_quotients_of s1),i) . n = H1 ./. N1
by A17, A18, A22, A33, FINSEQ_3:120;
verum end; end; hence
the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),
i
by A10, A2, A3, A9, A16, A18, A19, Def36;
verum