:: deftheorem defines AutGroup AUTGROUP:def 3 :
for G being strict Group holds AutGroup G = multMagma(# (Aut G),(AutComp G) #);