let G be Group; :: thesis: ( G is nilpotent iff ex F being FinSequence of the_normal_subgroups_of G st
( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( 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,((Omega). G).] is Subgroup of G2 ) ) ) )

A1: now :: thesis: ( G is nilpotent implies ex F being FinSequence of the_normal_subgroups_of G st
( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( 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,((Omega). G).] is Subgroup of G2 ) ) ) )

assume G is nilpotent ; :: thesis: ex F being FinSequence of the_normal_subgroups_of G st
( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( 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,((Omega). G).] is Subgroup of G2 ) ) )
then consider R being FinSequence of the_normal_subgroups_of G such that
A2: ( len R > 0 & R . 1 = (Omega). G & R . (len R) = (1). G & ( for i being Element of NAT st i in dom R & i + 1 in dom R holds
for H1, H2 being strict normal Subgroup of G st H1 = R . i & H2 = R . (i + 1) holds
( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) ) ) ;
reconsider F = R as FinSequence of the_normal_subgroups_of G ;
A3: 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 strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 )

proof

let i be Element of NAT ; :: thesis: ( i in dom F & i + 1 in dom F implies for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 ) )
assume A4: ( i in dom F & i + 1 in dom F ) ; :: thesis: for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 )
let G1, G2 be strict normal Subgroup of G; :: thesis: ( G1 = F . i & G2 = F . (i + 1) implies ( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 ) )
assume A5: ( G1 = F . i & G2 = F . (i + 1) ) ; :: thesis: ( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 )
then A6: ( G2 is strict Subgroup of G1 & ( for N being strict normal Subgroup of G st N = G2 & N is strict Subgroup of G1 holds
G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) ) ) by A2, A4;
[.G1,((Omega). G).] is strict Subgroup of G2

proof

now :: thesis: for N being strict normal Subgroup of G st N = G2 & N is strict Subgroup of G1 holds
[.G1,((Omega). G).] is strict Subgroup of G2

let N be strict normal Subgroup of G; :: thesis: ( N = G2 & N is strict Subgroup of G1 implies [.G1,((Omega). G).] is strict Subgroup of G2 )
assume A7: ( N = G2 & N is strict Subgroup of G1 ) ; :: thesis: [.G1,((Omega). G).] is strict Subgroup of G2
then G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) by A2, A4, A5;
hence [.G1,((Omega). G).] is strict Subgroup of G2 by A7, Th19; :: thesis: verum

end;

hence [.G1,((Omega). G).] is strict Subgroup of G2 by A6; :: thesis: verum

end;

hence ( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 ) by A2, A4, A5; :: thesis: verum

end;

take F = F; :: thesis: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( 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,((Omega). G).] is Subgroup of G2 ) ) )
thus ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( 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,((Omega). G).] is Subgroup of G2 ) ) ) by A2, A3; :: thesis: verum

end;

now :: thesis: ( ex F being FinSequence of the_normal_subgroups_of G st
( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( 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,((Omega). G).] is Subgroup of G2 ) ) ) implies ex F being FinSequence of the_normal_subgroups_of G st G is nilpotent )

given F being FinSequence of the_normal_subgroups_of G such that A8: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( 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,((Omega). G).] is Subgroup of G2 ) ) ) ; :: thesis: ex F being FinSequence of the_normal_subgroups_of G st G is nilpotent
A9: 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 strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) )

proof

let i be Element of NAT ; :: thesis: ( i in dom F & i + 1 in dom F implies for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) )
assume A10: ( i in dom F & i + 1 in dom F ) ; :: thesis: for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) )
let G1, G2 be strict normal Subgroup of G; :: thesis: ( G1 = F . i & G2 = F . (i + 1) implies ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) )
assume A11: ( G1 = F . i & G2 = F . (i + 1) ) ; :: thesis: ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) )
then A12: G2 is strict Subgroup of G1 by A8, A10;
[.G1,((Omega). G).] is strict Subgroup of G2 by A8, A10, A11;
hence ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) by A12, Th20; :: thesis: verum

end;

take F = F; :: thesis: G is nilpotent
( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( 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 A8, A9;
hence G is nilpotent ; :: thesis: verum

end;

hence ( G is nilpotent iff ex F being FinSequence of the_normal_subgroups_of G st
( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( 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,((Omega). G).] is Subgroup of G2 ) ) ) ) by A1; :: thesis: verum