take H = <*((Omega). G),((1). G)*>; :: thesis: ( H is Element of bool [:NAT,(the_stable_subgroups_of G):] & H is FinSequence of the_stable_subgroups_of G & H is composition_series )

( (Omega). G is Element of the_stable_subgroups_of G & (1). G is Element of the_stable_subgroups_of G ) by Def11;

then reconsider H = H as FinSequence of the_stable_subgroups_of G by FINSEQ_2:13;

A1: H . (len H) = H . 2 by FINSEQ_1:44

.= (1). G by FINSEQ_1:44 ;

A2: for i being Nat st i in dom H & i + 1 in dom H holds

for H1, H2 being StableSubgroup of G st H1 = H . i & H2 = H . (i + 1) holds

H2 is normal StableSubgroup of H1

hence ( H is Element of bool [:NAT,(the_stable_subgroups_of G):] & H is FinSequence of the_stable_subgroups_of G & H is composition_series ) by A1, A2, Def28; :: thesis: verum

( (Omega). G is Element of the_stable_subgroups_of G & (1). G is Element of the_stable_subgroups_of G ) by Def11;

then reconsider H = H as FinSequence of the_stable_subgroups_of G by FINSEQ_2:13;

A1: H . (len H) = H . 2 by FINSEQ_1:44

.= (1). G by FINSEQ_1:44 ;

A2: for i being Nat st i in dom H & i + 1 in dom H holds

for H1, H2 being StableSubgroup of G st H1 = H . i & H2 = H . (i + 1) holds

H2 is normal StableSubgroup of H1

proof

H . 1 = (Omega). G
by FINSEQ_1:44;
let i be Nat; :: thesis: ( i in dom H & i + 1 in dom H implies for H1, H2 being StableSubgroup of G st H1 = H . i & H2 = H . (i + 1) holds

H2 is normal StableSubgroup of H1 )

assume A3: i in dom H ; :: thesis: ( not i + 1 in dom H or for H1, H2 being StableSubgroup of G st H1 = H . i & H2 = H . (i + 1) holds

H2 is normal StableSubgroup of H1 )

assume A4: i + 1 in dom H ; :: thesis: for H1, H2 being StableSubgroup of G st H1 = H . i & H2 = H . (i + 1) holds

H2 is normal StableSubgroup of H1

len H = 2 by FINSEQ_1:44;

then A5: dom H = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;

end;H2 is normal StableSubgroup of H1 )

assume A3: i in dom H ; :: thesis: ( not i + 1 in dom H or for H1, H2 being StableSubgroup of G st H1 = H . i & H2 = H . (i + 1) holds

H2 is normal StableSubgroup of H1 )

assume A4: i + 1 in dom H ; :: thesis: for H1, H2 being StableSubgroup of G st H1 = H . i & H2 = H . (i + 1) holds

H2 is normal StableSubgroup of H1

len H = 2 by FINSEQ_1:44;

then A5: dom H = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;

per cases
( i = 1 or i = 2 )
by A3, A5, TARSKI:def 2;

end;

suppose A6:
i = 1
; :: thesis: for H1, H2 being StableSubgroup of G st H1 = H . i & H2 = H . (i + 1) holds

H2 is normal StableSubgroup of H1

H2 is normal StableSubgroup of H1

let H1, H2 be StableSubgroup of G; :: thesis: ( H1 = H . i & H2 = H . (i + 1) implies H2 is normal StableSubgroup of H1 )

assume H1 = H . i ; :: thesis: ( not H2 = H . (i + 1) or H2 is normal StableSubgroup of H1 )

assume H2 = H . (i + 1) ; :: thesis: H2 is normal StableSubgroup of H1

then A7: H2 = (1). G by A6, FINSEQ_1:44;

then reconsider H2 = H2 as StableSubgroup of H1 by Th16;

end;assume H1 = H . i ; :: thesis: ( not H2 = H . (i + 1) or H2 is normal StableSubgroup of H1 )

assume H2 = H . (i + 1) ; :: thesis: H2 is normal StableSubgroup of H1

then A7: H2 = (1). G by A6, FINSEQ_1:44;

then reconsider H2 = H2 as StableSubgroup of H1 by Th16;

now :: thesis: for H being strict Subgroup of H1 st multMagma(# the carrier of H2, the multF of H2 #) = H holds

H is normal

hence
H2 is normal StableSubgroup of H1
by Def10; :: thesis: verumH is normal

let H be strict Subgroup of H1; :: thesis: ( multMagma(# the carrier of H2, the multF of H2 #) = H implies H is normal )

reconsider H1 = H1 as Subgroup of G by Def7;

assume multMagma(# the carrier of H2, the multF of H2 #) = H ; :: thesis: H is normal

then the carrier of H = {(1_ G)} by A7, Def8;

then the carrier of H = {(1_ H1)} by GROUP_2:44;

then H = (1). H1 by GROUP_2:def 7;

hence H is normal ; :: thesis: verum

end;reconsider H1 = H1 as Subgroup of G by Def7;

assume multMagma(# the carrier of H2, the multF of H2 #) = H ; :: thesis: H is normal

then the carrier of H = {(1_ G)} by A7, Def8;

then the carrier of H = {(1_ H1)} by GROUP_2:44;

then H = (1). H1 by GROUP_2:def 7;

hence H is normal ; :: thesis: verum

suppose
i = 2
; :: thesis: for H1, H2 being StableSubgroup of G st H1 = H . i & H2 = H . (i + 1) holds

H2 is normal StableSubgroup of H1

H2 is normal StableSubgroup of H1

hence
for H1, H2 being StableSubgroup of G st H1 = H . i & H2 = H . (i + 1) holds

H2 is normal StableSubgroup of H1 by A4, A5, TARSKI:def 2; :: thesis: verum

end;H2 is normal StableSubgroup of H1 by A4, A5, TARSKI:def 2; :: thesis: verum

hence ( H is Element of bool [:NAT,(the_stable_subgroups_of G):] & H is FinSequence of the_stable_subgroups_of G & H is composition_series ) by A1, A2, Def28; :: thesis: verum