let I be non empty set ; :: thesis: for F being Group-Family of I
for S being normal Subgroup-Family of F holds product S is normal Subgroup of product F
let F be Group-Family of I; :: thesis: for S being normal Subgroup-Family of F holds product S is normal Subgroup of product F
let S be normal Subgroup-Family of F; :: thesis: product S is normal Subgroup of product F
for g being Element of (product F) holds (product S) |^ g is Subgroup of product S

proof

let g be Element of (product F); :: thesis: (product S) |^ g is Subgroup of product S
for h being Element of (product F) st h in (product S) |^ g holds
h in product S

proof

let h be Element of (product F); :: thesis: ( h in (product S) |^ g implies h in product S )
assume h in (product S) |^ g ; :: thesis: h in product S
then consider a being Element of (product F) such that
A2: ( h = a |^ g & a in product S ) by GROUP_3:58;
A3: dom h = I by GROUP_19:3;
for i being Element of I holds h . i in S . i

proof

let i be Element of I; :: thesis: h . i in S . i
h . i = (((g ") * a) * g) . i by A2, GROUP_3:def 2
.= (((g ") * a) /. i) * (g /. i) by GROUP_7:1
.= (((g ") /. i) * (a /. i)) * (g /. i) by GROUP_7:1
.= (((g /. i) ") * (a /. i)) * (g /. i) by GROUP_7:8
.= (a /. i) |^ (g /. i) by GROUP_3:def 2 ;
then h . i in (S . i) |^ (g /. i) by A2, GROUP_19:5, GROUP_3:58;
then h . i in multMagma(# the carrier of (S . i), the multF of (S . i) #) by GROUP_3:def 13;
hence h . i in S . i ; :: thesis: verum

end;

hence h in product S by A3, Th47; :: thesis: verum

end;

hence (product S) |^ g is Subgroup of product S by GROUP_2:58; :: thesis: verum

end;

hence product S is normal Subgroup of product F by GROUP_3:122; :: thesis: verum