let G be Group; :: thesis: for h, g being Element of G st ( h * g = h or g * h = h ) holds
g = 1_ G
let h, g be Element of G; :: thesis: ( ( h * g = h or g * h = h ) implies g = 1_ G )
( h * (1_ G) = h & (1_ G) * h = h ) by Def5;
hence ( ( h * g = h or g * h = h ) implies g = 1_ G ) by Th14; :: thesis: verum