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