theorem :: AUTGROUP:28

for G being Group
for f being Element of InnAut G holds
( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f )