let I be non empty set ; :: thesis: for G being Group
for J being non empty Subset of I
for F being normal Subgroup-Family of I,G holds F | J is normal Subgroup-Family of J,G
let G be Group; :: thesis: for J being non empty Subset of I
for F being normal Subgroup-Family of I,G holds F | J is normal Subgroup-Family of J,G
let J be non empty Subset of I; :: thesis: for F being normal Subgroup-Family of I,G holds F | J is normal Subgroup-Family of J,G
let F be normal Subgroup-Family of I,G; :: thesis: F | J is normal Subgroup-Family of J,G
for j being Element of J holds (F | J) . j is normal Subgroup of G

proof

let j be Element of J; :: thesis: (F | J) . j is normal Subgroup of G
j in J ;
then j in dom (F | J) by PARTFUN1:def 2;
then F . j = (F | J) . j by FUNCT_1:47;
hence (F | J) . j is normal Subgroup of G ; :: thesis: verum

end;

hence F | J is normal Subgroup-Family of J,G by ThS1; :: thesis: verum