:: deftheorem Def3 defines Group-like GROUP_7:def 3 :
for I being set
for F being multMagma-Family of I holds
( F is Group-like iff for i being set st i in I holds
ex Fi being non empty Group-like multMagma st Fi = F . i );