now :: thesis: ( 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 ; :: thesis: 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 S₁[ 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 S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg i implies ex x being object st S₁[k,x] )
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
assume A2: k in Seg i ; :: thesis: ex x being object st S₁[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 ; :: thesis: S₁[k,H ./. N]
thus S₁[k,H ./. N] ; :: thesis: verum

end;

consider f being FinSequence such that
A7: ( dom f = Seg i & ( for k being Nat st k in Seg i holds
S₁[k,f . k] ) ) from FINSEQ_1:sch 1(A1);
take f = f; :: thesis: ( 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 ; :: thesis: 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
let j be Nat; :: thesis: ( 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 ; :: thesis: 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
let H be StableSubgroup of G; :: thesis: for N being normal StableSubgroup of H st H = s . j & N = s . (j + 1) holds
f . j = H ./. N
let N be normal StableSubgroup of H; :: thesis: ( H = s . j & N = s . (j + 1) implies f . j = H ./. N )
assume A9: H = s . j ; :: thesis: ( N = s . (j + 1) implies f . j = H ./. N )
assume N = s . (j + 1) ; :: thesis: f . j = H ./. N
hence f . j = H ./. N by A7, A8, A9; :: thesis: verum

end;

hence ( ( len s > 1 implies ex b₁ being FinSequence st
( len s = (len b₁) + 1 & ( for i being Nat st i in dom b₁ holds
for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds
b₁ . i = H ./. N ) ) ) & ( not len s > 1 implies ex b₁ being FinSequence st b₁ = {} ) ) ; :: thesis: verum