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