let f1, f2 be FinSequence; :: thesis: ( ( len s > 1 & len s = (len f1) + 1 & ( for i being Nat st i in dom f1 holds

for H being StableSubgroup of G

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

f1 . i = H ./. N ) & len s = (len f2) + 1 & ( for i being Nat st i in dom f2 holds

for H being StableSubgroup of G

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

f2 . i = H ./. N ) implies f1 = f2 ) & ( not len s > 1 & f1 = {} & f2 = {} implies f1 = f2 ) )

for H being StableSubgroup of G

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

f1 . i = H ./. N ) & len s = (len f2) + 1 & ( for i being Nat st i in dom f2 holds

for H being StableSubgroup of G

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

f2 . i = H ./. N ) implies f1 = f2 ) & ( not len s > 1 & f1 = {} & f2 = {} implies f1 = f2 ) ) ; :: thesis: verum

for H being StableSubgroup of G

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

f1 . i = H ./. N ) & len s = (len f2) + 1 & ( for i being Nat st i in dom f2 holds

for H being StableSubgroup of G

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

f2 . i = H ./. N ) implies f1 = f2 ) & ( not len s > 1 & f1 = {} & f2 = {} implies f1 = f2 ) )

now :: thesis: ( len s > 1 & len s = (len f1) + 1 & ( for i being Nat st i in dom f1 holds

for H1 being StableSubgroup of G

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

f1 . i = H1 ./. N1 ) & len s = (len f2) + 1 & ( for i being Nat st i in dom f2 holds

for H1 being StableSubgroup of G

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

f2 . i = H1 ./. N1 ) implies f1 = f2 )

hence
( ( len s > 1 & len s = (len f1) + 1 & ( for i being Nat st i in dom f1 holds for H1 being StableSubgroup of G

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

f1 . i = H1 ./. N1 ) & len s = (len f2) + 1 & ( for i being Nat st i in dom f2 holds

for H1 being StableSubgroup of G

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

f2 . i = H1 ./. N1 ) implies f1 = f2 )

assume
len s > 1
; :: thesis: ( len s = (len f1) + 1 & ( for i being Nat st i in dom f1 holds

for H1 being StableSubgroup of G

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

f1 . i = H1 ./. N1 ) & len s = (len f2) + 1 & ( for i being Nat st i in dom f2 holds

for H1 being StableSubgroup of G

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

f2 . i = H1 ./. N1 ) implies f1 = f2 )

assume A10: len s = (len f1) + 1 ; :: thesis: ( ( for i being Nat st i in dom f1 holds

for H1 being StableSubgroup of G

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

f1 . i = H1 ./. N1 ) & len s = (len f2) + 1 & ( for i being Nat st i in dom f2 holds

for H1 being StableSubgroup of G

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

f2 . i = H1 ./. N1 ) implies f1 = f2 )

assume A11: for i being Nat st i in dom f1 holds

for H1 being StableSubgroup of G

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

f1 . i = H1 ./. N1 ; :: thesis: ( len s = (len f2) + 1 & ( for i being Nat st i in dom f2 holds

for H1 being StableSubgroup of G

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

f2 . i = H1 ./. N1 ) implies f1 = f2 )

assume A12: len s = (len f2) + 1 ; :: thesis: ( ( for i being Nat st i in dom f2 holds

for H1 being StableSubgroup of G

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

f2 . i = H1 ./. N1 ) implies f1 = f2 )

assume A13: for i being Nat st i in dom f2 holds

for H1 being StableSubgroup of G

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

f2 . i = H1 ./. N1 ; :: thesis: f1 = f2

for k being Nat st 1 <= k & k <= len f1 holds

f1 . k = f2 . k

end;for H1 being StableSubgroup of G

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

f1 . i = H1 ./. N1 ) & len s = (len f2) + 1 & ( for i being Nat st i in dom f2 holds

for H1 being StableSubgroup of G

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

f2 . i = H1 ./. N1 ) implies f1 = f2 )

assume A10: len s = (len f1) + 1 ; :: thesis: ( ( for i being Nat st i in dom f1 holds

for H1 being StableSubgroup of G

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

f1 . i = H1 ./. N1 ) & len s = (len f2) + 1 & ( for i being Nat st i in dom f2 holds

for H1 being StableSubgroup of G

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

f2 . i = H1 ./. N1 ) implies f1 = f2 )

assume A11: for i being Nat st i in dom f1 holds

for H1 being StableSubgroup of G

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

f1 . i = H1 ./. N1 ; :: thesis: ( len s = (len f2) + 1 & ( for i being Nat st i in dom f2 holds

for H1 being StableSubgroup of G

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

f2 . i = H1 ./. N1 ) implies f1 = f2 )

assume A12: len s = (len f2) + 1 ; :: thesis: ( ( for i being Nat st i in dom f2 holds

for H1 being StableSubgroup of G

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

f2 . i = H1 ./. N1 ) implies f1 = f2 )

assume A13: for i being Nat st i in dom f2 holds

for H1 being StableSubgroup of G

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

f2 . i = H1 ./. N1 ; :: thesis: f1 = f2

for k being Nat st 1 <= k & k <= len f1 holds

f1 . k = f2 . k

proof

hence
f1 = f2
by A10, A12; :: thesis: verum
let k be Nat; :: thesis: ( 1 <= k & k <= len f1 implies f1 . k = f2 . k )

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

assume that

A14: 1 <= k and

A15: k <= len f1 ; :: thesis: f1 . k = f2 . k

A16: k + 1 <= ((len s) - 1) + 1 by A10, A15, XREAL_1:6;

0 + k <= 1 + k by XREAL_1:6;

then k <= len s by A16, XXREAL_0:2;

then k1 in Seg (len s) by A14;

then A17: k in dom s by FINSEQ_1:def 3;

1 + 1 <= k + 1 by A14, XREAL_1:6;

then 1 <= k + 1 by XXREAL_0:2;

then k1 + 1 in Seg (len s) by A16;

then A18: k + 1 in dom s by FINSEQ_1:def 3;

then reconsider H1 = s . k, N1 = s . (k + 1) as Element of the_stable_subgroups_of G by A17, FINSEQ_2:11;

reconsider H1 = H1, N1 = N1 as StableSubgroup of G by Def11;

reconsider N1 = N1 as normal StableSubgroup of H1 by A17, A18, Def28;

A19: k1 in Seg (len f1) by A14, A15;

then k in dom f1 by FINSEQ_1:def 3;

then A20: f1 . k = H1 ./. N1 by A11;

k in dom f2 by A10, A12, A19, FINSEQ_1:def 3;

hence f1 . k = f2 . k by A13, A20; :: thesis: verum

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

assume that

A14: 1 <= k and

A15: k <= len f1 ; :: thesis: f1 . k = f2 . k

A16: k + 1 <= ((len s) - 1) + 1 by A10, A15, XREAL_1:6;

0 + k <= 1 + k by XREAL_1:6;

then k <= len s by A16, XXREAL_0:2;

then k1 in Seg (len s) by A14;

then A17: k in dom s by FINSEQ_1:def 3;

1 + 1 <= k + 1 by A14, XREAL_1:6;

then 1 <= k + 1 by XXREAL_0:2;

then k1 + 1 in Seg (len s) by A16;

then A18: k + 1 in dom s by FINSEQ_1:def 3;

then reconsider H1 = s . k, N1 = s . (k + 1) as Element of the_stable_subgroups_of G by A17, FINSEQ_2:11;

reconsider H1 = H1, N1 = N1 as StableSubgroup of G by Def11;

reconsider N1 = N1 as normal StableSubgroup of H1 by A17, A18, Def28;

A19: k1 in Seg (len f1) by A14, A15;

then k in dom f1 by FINSEQ_1:def 3;

then A20: f1 . k = H1 ./. N1 by A11;

k in dom f2 by A10, A12, A19, FINSEQ_1:def 3;

hence f1 . k = f2 . k by A13, A20; :: thesis: verum

for H being StableSubgroup of G

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

f1 . i = H ./. N ) & len s = (len f2) + 1 & ( for i being Nat st i in dom f2 holds

for H being StableSubgroup of G

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

f2 . i = H ./. N ) implies f1 = f2 ) & ( not len s > 1 & f1 = {} & f2 = {} implies f1 = f2 ) ) ; :: thesis: verum