theorem :: GROUP_1:5

for G being Group
for g, h being Element of G st h * g = 1_ G & g * h = 1_ G holds
g = h " by Def5;