let I be non empty set ; :: thesis: for F being Group-Family of I ex S being componentwise_strict normal Subgroup-Family of F st
for i being Element of I holds S . i = (F . i) `
let F be Group-Family of I; :: thesis: ex S being componentwise_strict normal Subgroup-Family of F st
for i being Element of I holds S . i = (F . i) `
deffunc H₁( Group) -> Subgroup of $1 = $1 ` ;
A1: for G being Group holds H₁(G) is strict Subgroup of G ;
consider S being componentwise_strict Subgroup-Family of F such that
A2: for i being Element of I holds S . i = H₁(F . i) from GROUP_23:sch 3(A1);
for i being Element of I holds S . i is normal Subgroup of F . i

proof

let i be Element of I; :: thesis: S . i is normal Subgroup of F . i
S . i = (F . i) ` by A2;
hence S . i is normal Subgroup of F . i ; :: thesis: verum

end;

then reconsider S = S as componentwise_strict normal Subgroup-Family of F by Def7;
take S ; :: thesis: for i being Element of I holds S . i = (F . i) `
thus for i being Element of I holds S . i = (F . i) ` by A2; :: thesis: verum