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