theorem Th4: :: GROUP_12:4

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