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

B1: now

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
A1: ( 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) ) ) ) by def3;
reconsider F = R as FinSequence of the_normal_subgroups_of G ;
A2: 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 A3: ( 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 A4: ( G1 = F . i & G2 = F . (i + 1) ) ; :: thesis: ( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 )
then A5: ( 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 A1, A3;
[.G1,((Omega). G).] is strict Subgroup of G2

proof

now

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 A6: ( 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 A1, A3, A4;
hence [.G1,((Omega). G).] is strict Subgroup of G2 by A6, Th22; :: thesis: verum

end;

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

end;

hence ( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 ) by A1, A3, A4; :: 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 A1, A2; :: thesis: verum

end;

now

given F being FinSequence of the_normal_subgroups_of G such that A1: ( 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
A2: 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 A3: ( 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 A4: ( G1 = F . i & G2 = F . (i + 1) ) ; :: thesis: ( G2 is strict Subgroup of G1 & G1 ./. (G1,G2 `*` ) is Subgroup of center (G ./. G2) )
A5: G2 is strict Subgroup of G1 by A1, A3, A4;
[.G1,((Omega). G).] is strict Subgroup of G2 by A1, A3, A4;
hence ( G2 is strict Subgroup of G1 & G1 ./. (G1,G2 `*` ) is Subgroup of center (G ./. G2) ) by A5, Th24; :: 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 A1, A2;
hence G is nilpotent by def3; :: 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 B1; :: thesis: verum