:: deftheorem defines * ABSRED_0:def 35 :
for S being non empty partial quasi_total non-empty Group-like TRSStr
for a, b being Element of S holds a * b = (Den ((In (3,(dom the charact of S))),S)) . <*a,b*>;