for I being non empty set
for G being Group
for F being Group-Family of I st ( for i being Element of I holds F . i is Subgroup of G ) holds
1_ (product F) = I --> (1_ G)