theorem Th17: :: GROUP_3:17

for G being Group
for a being Element of G holds (1_ G) |^ a = 1_ G