theorem Th8: :: GROUP_7:8

for i, I being set
for f, g being Function
for F being Group-like associative multMagma-Family of I
for x being Element of (product F)
for G being Group
for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds
g . i = y "