take H = <*(),((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
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 ;
per cases ( i = 1 or i = 2 ) by ;
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 ;
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 ;
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 ; :: thesis: verum
end;
end;
end;
H . 1 = (Omega). G by FINSEQ_1:44;
hence ( H is Element of bool & H is FinSequence of the_stable_subgroups_of G & H is composition_series ) by ; :: thesis: verum