now ( len s > 1 implies ex f being FinSequence st
( len s = (len f) + 1 & ( for j being Nat st j in dom f holds
for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = s . j & N = s . (j + 1) holds
f . j = H ./. N ) ) )set i =
(len s) - 1;
assume
len s > 1
;
ex f being FinSequence st
( len s = (len f) + 1 & ( for j being Nat st j in dom f holds
for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = s . j & N = s . (j + 1) holds
f . j = H ./. N ) )then
(len s) - 1
> 1
- 1
by XREAL_1:9;
then reconsider i =
(len s) - 1 as
Element of
NAT by INT_1:3;
defpred S1[
set ,
object ]
means for
H being
StableSubgroup of
G for
N being
normal StableSubgroup of
H for
j being
Nat st $1
in Seg i &
j = $1 &
H = s . j &
N = s . (j + 1) holds
$2
= H ./. N;
A1:
for
k being
Nat st
k in Seg i holds
ex
x being
object st
S1[
k,
x]
proof
let k be
Nat;
( k in Seg i implies ex x being object st S1[k,x] )
reconsider k1 =
k as
Element of
NAT by ORDINAL1:def 12;
assume A2:
k in Seg i
;
ex x being object st S1[k,x]
then A3:
1
<= k
by FINSEQ_1:1;
k <= i
by A2, FINSEQ_1:1;
then A4:
k + 1
<= ((len s) - 1) + 1
by XREAL_1:6;
0 + k <= 1
+ k
by XREAL_1:6;
then
k <= len s
by A4, XXREAL_0:2;
then
k1 in Seg (len s)
by A3;
then A5:
k in dom s
by FINSEQ_1:def 3;
1
+ 1
<= k + 1
by A3, XREAL_1:6;
then
1
<= k + 1
by XXREAL_0:2;
then
k1 + 1
in Seg (len s)
by A4;
then A6:
k + 1
in dom s
by FINSEQ_1:def 3;
then reconsider H =
s . k,
N =
s . (k + 1) as
Element of
the_stable_subgroups_of G by A5, FINSEQ_2:11;
reconsider H =
H,
N =
N as
StableSubgroup of
G by Def11;
reconsider N =
N as
normal StableSubgroup of
H by A5, A6, Def28;
take
H ./. N
;
S1[k,H ./. N]
thus
S1[
k,
H ./. N]
;
verum
end; consider f being
FinSequence such that A7:
(
dom f = Seg i & ( for
k being
Nat st
k in Seg i holds
S1[
k,
f . k] ) )
from FINSEQ_1:sch 1(A1);
take f =
f;
( len s = (len f) + 1 & ( for j being Nat st j in dom f holds
for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = s . j & N = s . (j + 1) holds
f . j = H ./. N ) )
len f = i
by A7, FINSEQ_1:def 3;
hence
len s = (len f) + 1
;
for j being Nat st j in dom f holds
for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = s . j & N = s . (j + 1) holds
f . j = H ./. Nlet j be
Nat;
( j in dom f implies for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = s . j & N = s . (j + 1) holds
f . j = H ./. N )assume A8:
j in dom f
;
for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = s . j & N = s . (j + 1) holds
f . j = H ./. Nlet H be
StableSubgroup of
G;
for N being normal StableSubgroup of H st H = s . j & N = s . (j + 1) holds
f . j = H ./. Nlet N be
normal StableSubgroup of
H;
( H = s . j & N = s . (j + 1) implies f . j = H ./. N )assume A9:
H = s . j
;
( N = s . (j + 1) implies f . j = H ./. N )assume
N = s . (j + 1)
;
f . j = H ./. Nhence
f . j = H ./. N
by A7, A8, A9;
verum end;
hence
( ( len s > 1 implies ex b1 being FinSequence st
( len s = (len b1) + 1 & ( for i being Nat st i in dom b1 holds
for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds
b1 . i = H ./. N ) ) ) & ( not len s > 1 implies ex b1 being FinSequence st b1 = {} ) )
; verum