let G be Group; :: thesis: for a, b, g being Element of G st a |^ g = b |^ g holds
a = b
let a, b, g be Element of G; :: thesis: ( a |^ g = b |^ g implies a = b )
assume a |^ g = b |^ g ; :: thesis: a = b
then (g ") * a = (g ") * b by GROUP_1:6;
hence a = b by GROUP_1:6; :: thesis: verum