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 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 )set i =
(len s) - 1;
assume A18:
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 A19:
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 A20:
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 A21:
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 13;
assume A22:
( 1
<= k &
k <= len f1 )
;
:: thesis: f1 . k = f2 . k
then A23:
k1 in Seg (len f1)
;
then A24:
k in dom f1
by FINSEQ_1:def 3;
A25:
k in dom f2
by A18, A20, A23, FINSEQ_1:def 3;
A26:
k + 1
<= ((len s) - 1) + 1
by A18, A22, XREAL_1:8;
1
+ 1
<= k + 1
by A22, XREAL_1:8;
then A27:
1
<= k + 1
by XXREAL_0:2;
0 + k <= 1
+ k
by XREAL_1:8;
then
k <= len s
by A26, XXREAL_0:2;
then
(
k1 in Seg (len s) &
k1 + 1
in Seg (len s) )
by A22, A26, A27;
then A28:
(
k in dom s &
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 FINSEQ_2:13;
reconsider H1 =
H1,
N1 =
N1 as
StableSubgroup of
G by Def11;
reconsider N1 =
N1 as
normal StableSubgroup of
H1 by A28, Def31;
f1 . k = H1 ./. N1
by A19, A24;
hence
f1 . k = f2 . k
by A21, A25;
:: thesis: verum
end; hence
f1 = f2
by A18, A20, FINSEQ_1:18;
:: 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