for G being Group
for F being FinSequence of the_normal_subgroups_of G
for j being Element of NAT st j in dom F holds
F . j is strict normal Subgroup of G