consider F being FinSequence of the_normal_subgroups_of G such that
A1: len F > 0 and
A2: F . 1 = (Omega). G and
A3: F . (len F) = (1). G and
A4: for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) by Def2;
1 <= len F by A1, NAT_1:14;
then A5: 1 in Seg (len F) ;
defpred S₁[ set , set ] means ex J being strict normal Subgroup of G st
( J = F . G & H = h .: J );
A6: for k being Nat st k in Seg (len F) holds
ex x being Element of the_normal_subgroups_of (Image h) st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len F) implies ex x being Element of the_normal_subgroups_of (Image h) st S₁[k,x] )
assume k in Seg (len F) ; :: thesis: ex x being Element of the_normal_subgroups_of (Image h) st S₁[k,x]
then k in dom F by FINSEQ_1:def 3;
then F . k in the_normal_subgroups_of G by FINSEQ_2:11;
then F . k is strict normal Subgroup of G by Def1;
then consider A being strict normal Subgroup of G such that
A7: A = F . k ;
h .: A is strict normal Subgroup of Image h by Th26;
then h .: A in the_normal_subgroups_of (Image h) by Def1;
hence ex x being Element of the_normal_subgroups_of (Image h) st S₁[k,x] by A7; :: thesis: verum

end;

consider Z being FinSequence of the_normal_subgroups_of (Image h) such that
A8: ( dom Z = Seg (len F) & ( for j being Nat st j in Seg (len F) holds
S₁[j,Z . j] ) ) from FINSEQ_1:sch 5(A6);
Seg (len Z) = Seg (len F) by A8, FINSEQ_1:def 3;
then A9: dom F = Seg (len Z) by FINSEQ_1:def 3
.= dom Z by FINSEQ_1:def 3 ;
A10: for i being Element of NAT st i in dom Z & i + 1 in dom Z holds
for H1, H2 being strict normal Subgroup of Image h st H1 = Z . i & H2 = Z . (i + 1) holds
( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) )

proof

let i be Element of NAT ; :: thesis: ( i in dom Z & i + 1 in dom Z implies for H1, H2 being strict normal Subgroup of Image h st H1 = Z . i & H2 = Z . (i + 1) holds
( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) ) )
assume A11: ( i in dom Z & i + 1 in dom Z ) ; :: thesis: for H1, H2 being strict normal Subgroup of Image h st H1 = Z . i & H2 = Z . (i + 1) holds
( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) )
let H1, H2 be strict normal Subgroup of Image h; :: thesis: ( H1 = Z . i & H2 = Z . (i + 1) implies ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) ) )
assume that
A12: H1 = Z . i and
A13: H2 = Z . (i + 1) ; :: thesis: ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) )
A14: ( i in dom F & i + 1 in dom F ) by A8, A11, FINSEQ_1:def 3;
consider G1 being strict normal Subgroup of G such that
A15: G1 = F . i and
A16: H1 = h .: G1 by A8, A11, A12;
consider G2 being strict normal Subgroup of G such that
A17: G2 = F . (i + 1) and
A18: H2 = h .: G2 by A8, A11, A13;
A19: G2 is strict Subgroup of G1 by A4, A9, A11, A15, A17;
G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) by A14, A15, A17, A4;
hence ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) ) by A16, A19, A18, Th25, GRSOLV_1:12; :: thesis: verum

end;

take Z ; :: according to GRNILP_1:def 2 :: thesis: ( len Z > 0 & Z . 1 = (Omega). (Image h) & Z . (len Z) = (1). (Image h) & ( for i being Element of NAT st i in dom Z & i + 1 in dom Z holds
for G1, G2 being strict normal Subgroup of Image h st G1 = Z . i & G2 = Z . (i + 1) holds
( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center ((Image h) ./. G2) ) ) )
A20: len Z = len F by A8, FINSEQ_1:def 3;
( Z . 1 = (Omega). (Image h) & Z . (len Z) = (1). (Image h) )

proof

ex G1 being strict normal Subgroup of G st
( G1 = F . 1 & Z . 1 = h .: G1 ) by A8, A5;
hence Z . 1 = (Omega). (Image h) by A2, GRSOLV_1:11; :: thesis: Z . (len Z) = (1). (Image h)
ex G2 being strict normal Subgroup of G st
( G2 = F . (len F) & Z . (len F) = h .: G2 ) by A1, A8, FINSEQ_1:3;
hence Z . (len Z) = (1). H by A3, A20, GRSOLV_1:11
.= (1). (Image h) by GROUP_2:63 ;
:: thesis: verum

end;

hence ( len Z > 0 & Z . 1 = (Omega). (Image h) & Z . (len Z) = (1). (Image h) & ( for i being Element of NAT st i in dom Z & i + 1 in dom Z holds
for G1, G2 being strict normal Subgroup of Image h st G1 = Z . i & G2 = Z . (i + 1) holds
( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center ((Image h) ./. G2) ) ) ) by A1, A8, A10, FINSEQ_1:def 3; :: thesis: verum