theorem :: GROUP_19:14

for I being non empty set
for F being Group-Family of I
for G being Group
for x being finite-support Function of I,G st support x = {} & ( for i being object st i in I holds
F . i is Subgroup of G ) holds
x = 1_ (product F)