theorem Th3: :: GROUP_12:3

for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for g1, g2 being Element of (product F)
for z1, z2 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) holds
g1 * g2 = (1_ (product F)) +* (i,(z1 * z2))