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