theorem Th5: :: GROUP_7:5

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