:: deftheorem Def2 defines AutComp AUTGROUP:def 2 :
for G being strict Group
for b₂ being BinOp of (Aut G) holds
( b₂ = AutComp G iff for x, y being Element of Aut G holds b₂ . (x,y) = x * y );