let I be non empty set ; :: thesis: for F being Group-Family of I
for D being Subgroup-Family of F st ( for i being Element of I holds D . i = (F . i) ` ) holds
(product F) ` is strict Subgroup of product D
let F be Group-Family of I; :: thesis: for D being Subgroup-Family of F st ( for i being Element of I holds D . i = (F . i) ` ) holds
(product F) ` is strict Subgroup of product D
let D be Subgroup-Family of F; :: thesis: ( ( for i being Element of I holds D . i = (F . i) ` ) implies (product F) ` is strict Subgroup of product D )
assume A1: for i being Element of I holds D . i = (F . i) ` ; :: thesis: (product F) ` is strict Subgroup of product D
for a, b being Element of (product F) holds [.a,b.] in product D

proof

let a, b be Element of (product F); :: thesis: [.a,b.] in product D
B1: dom [.a,b.] = I by GROUP_19:3;
for i being Element of I holds [.a,b.] . i in D . i

proof

let i be Element of I; :: thesis: [.a,b.] . i in D . i
( a /. i in (Omega). (F . i) & b /. i in (Omega). (F . i) ) ;
then [.(a /. i),(b /. i).] in [.((Omega). (F . i)),((Omega). (F . i)).] by GROUP_5:65;
then [.(a /. i),(b /. i).] in (F . i) ` by GROUP_5:def 9;
then [.a,b.] . i in (F . i) ` by Th57;
hence [.a,b.] . i in D . i by A1; :: thesis: verum

end;

hence [.a,b.] in product D by B1, Th47; :: thesis: verum

end;

hence (product F) ` is strict Subgroup of product D by GROUP_6:7; :: thesis: verum