:: deftheorem defines con_class GROUP_1A:def 36 :
for G being addGroup
for a being Element of G holds con_class a = a * (carr ((Omega). G));