let G be Group; :: thesis: for I being set
for J being Subset of I
for F being normal Subgroup-Family of I,G holds F | J is normal Subgroup-Family of J,G
let I be set ; :: thesis: for J being 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 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 i being object st i in J holds
(F | J) . i is normal Subgroup of G

proof

let i be object ; :: thesis: ( i in J implies (F | J) . i is normal Subgroup of G )
assume A1: i in J ; :: thesis: (F | J) . i is normal Subgroup of G
then A2: F . i is normal Subgroup of G by Def18;
dom (F | J) = J by PARTFUN1:def 2;
hence (F | J) . i is normal Subgroup of G by A1, A2, FUNCT_1:47; :: thesis: verum

end;

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