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 A1: h * (g ") = 1_ G by Def6;
g * (g ") = 1_ G by Def6;
hence h = g by A1, Th14; :: thesis: verum