let G be Group; :: thesis: for a, g, b being Element of G st a |^ g = b |^ g holds
a = b
let a, g, b 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:14;
hence a = b by GROUP_1:14; :: thesis: verum