theorem Th29: :: GROUP_23:32

for I being non empty set
for i being Element of I
for F being Group-Family of I
for g being Element of (product F) holds g . i is Element of (F . i)