:: deftheorem defines (Omega). GROUP_2:def 8 :
for G being Group holds (Omega). G = multMagma(# the carrier of G, the multF of G #);