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