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