theorem Th19: :: GROUP_3:19

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