theorem Th6: :: GROUP_7:6

for i, I being set
for f being Function
for F being Group-like multMagma-Family of I
for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds
f . i = 1_ G