:: deftheorem defines MSAAutGroup AUTALG_1:def 7 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S holds MSAAutGroup U1 = multMagma(# (MSAAut U1),(MSAAutComp U1) #);