let G be Group; :: thesis: 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
let F be FinSequence of the_normal_subgroups_of G; :: thesis: for j being Element of NAT st j in dom F holds
F . j is strict normal Subgroup of G
let j be Element of NAT ; :: thesis: ( j in dom F implies F . j is strict normal Subgroup of G )
assume j in dom F ; :: thesis: F . j is strict normal Subgroup of G
then F . j in rng F by FUNCT_1:3;
hence F . j is strict normal Subgroup of G by Def1; :: thesis: verum