for G being Group
for F being FinSequence of the_normal_subgroups_of G holds F is FinSequence of Subgroups G