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

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 )
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
proof
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 ;
0 + k <= 1 + k by XREAL_1:6;
then k <= len s by ;
then k1 in Seg (len s) by A14;
then A17: 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 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 ;
reconsider H1 = H1, N1 = N1 as StableSubgroup of G by Def11;
reconsider N1 = N1 as normal StableSubgroup of H1 by ;
A19: k1 in Seg (len f1) by ;
then k in dom f1 by FINSEQ_1:def 3;
then A20: f1 . k = H1 ./. N1 by A11;
k in dom f2 by ;
hence f1 . k = f2 . k by ; :: thesis: verum
end;
hence f1 = f2 by ; :: thesis: verum
end;
hence ( ( 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 ) ) ; :: thesis: verum