let G be Group; :: thesis: for F being FinSequence of the_normal_subgroups_of G holds F is FinSequence of Subgroups G
let F be FinSequence of the_normal_subgroups_of G; :: thesis: F is FinSequence of Subgroups G
the_normal_subgroups_of G c= Subgroups G by Th17;
then rng F c= Subgroups G ;
hence F is FinSequence of Subgroups G by FINSEQ_1:def 4; :: thesis: verum