let I be non empty finite 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) ` = 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) ` = product D
let D be Subgroup-Family of F; :: thesis: ( ( for i being Element of I holds D . i = (F . i) ` ) implies (product F) ` = product D )
assume A1: for i being Element of I holds D . i = (F . i) ` ; :: thesis: (product F) ` = product D
sum D = product D by GROUP_7:9;
then A2: product D is strict Subgroup of (product F) ` by A1, Th62;
(product F) ` is strict Subgroup of product D by A1, Th61;
hence (product F) ` = product D by A2, GROUP_2:55; :: thesis: verum