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

hence f1 = f2 by A10, A12; :: 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