theorem :: AUTGROUP:30
for G being Group st G is commutative Group holds
for f being Element of (InnAutGroup G) holds f = 1_ (InnAutGroup G)