let f1, f2 be FinSequence; ( ( 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 ( 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
;
( 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
;
( ( 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
;
( 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
;
( ( 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
;
f1 = f2
for
k being
Nat st 1
<= k &
k <= len f1 holds
f1 . k = f2 . k
proof
let k be
Nat;
( 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
;
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;
verum
end; hence
f1 = f2
by A10, A12;
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 ) )
; verum