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