:: deftheorem Def1 defines Aut AUTGROUP:def 1 :
for G being strict Group
for b₂ being FUNCTION_DOMAIN of the carrier of G, the carrier of G holds
( b₂ = Aut G iff ( ( for f being Element of b₂ holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in b₂ iff ( h is one-to-one & h is onto ) ) ) ) );