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 ) ) )

hence
( ( len s > 1 implies ex b( 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_{1}[ 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_{1}[k,x]

A7: ( dom f = Seg i & ( for k being Nat st k in Seg i holds

S_{1}[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;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

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

proof

consider f being FinSequence such that
let k be Nat; :: thesis: ( k in Seg i implies ex x being object st S_{1}[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_{1}[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_{1}[k,H ./. N]

thus S_{1}[k,H ./. N]
; :: thesis: verum

end;reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

assume A2: k in Seg i ; :: thesis: ex x being object st S

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

thus S

A7: ( dom f = Seg i & ( for k being Nat st k in Seg i holds

S

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

( len s = (len b

for H being StableSubgroup of G

for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds

b