:: deftheorem defines UAAutGroup AUTALG_1:def 3 :
for UA being Universal_Algebra holds UAAutGroup UA = multMagma(# (UAAut UA),(UAAutComp UA) #);