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 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; :: thesis: ( 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 ; :: thesis: ex x being object st S1[k,x]
then A3: 1 <= k by FINSEQ_1:1;
k <= i by ;
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 ;
then k1 in Seg (len s) by A3;
then A5: k in dom s by FINSEQ_1:def 3;
1 + 1 <= k + 1 by ;
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 ;
reconsider H = H, N = N as StableSubgroup of G by Def11;
reconsider N = N as normal StableSubgroup of H by ;
take H ./. N ; :: thesis: S1[k,H ./. N]
thus S1[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
S1[k,f . k] ) ) from 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 ;
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 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 = {} ) ) ; :: thesis: verum