:: deftheorem Def4 defines InnAut AUTGROUP:def 4 :
for G being strict Group
for b₂ being FUNCTION_DOMAIN of the carrier of G, the carrier of G holds
( b₂ = InnAut G iff for f being Element of Funcs ( the carrier of G, the carrier of G) holds
( f in b₂ iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a ) );