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

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;

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

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

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

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;

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

end;

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

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;

end;

end;

H . 1 = (Omega). G ;
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