theorem Th23: :: AUTGROUP:23

for G being Group
for a being Element of G holds (Conjugate (1_ G)) . a = a