:: deftheorem Def7 defines associative GROUP_7:def 7 :
for I being non empty set
for F being multMagma-Family of I holds
( F is associative iff for i being Element of I holds F . i is associative );