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