take H = <*((Omega). G),((1). G)*>; :: thesis:
( (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

let i be Nat; :: thesis:
assume A3: i in dom H ; :: thesis:
assume A4: i + 1 in dom H ; :: thesis:
len H = 2 by FINSEQ_1:44;
then A5: dom H = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;

per cases by A3, A5, TARSKI:def 2;

suppose A6: i = 1 ; :: thesis:

let H1, H2 be StableSubgroup of G; :: thesis:
assume H1 = H . i ; :: thesis:
assume H2 = H . (i + 1) ; :: thesis:
then A7: H2 = (1). G by A6, FINSEQ_1:44;
then reconsider H2 = H2 as StableSubgroup of H1 by Th16;

let H be strict Subgroup of H1; :: thesis:
reconsider H1 = H1 as Subgroup of G by Def7;
assume multMagma(# the carrier of H2, the multF of H2 #) = H ; :: thesis:
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:

end;

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

end;

suppose i = 2 ; :: thesis:

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:

end;

end;

end;

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