let G be Group; :: thesis: for f, g, h being Element of G st ( h * g = h * f or g * h = f * h ) holds
g = f
let f, g, h 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 Def3;
then ( (h ") * (h * g) = (1_ G) * f or g * (h * (h ")) = f * (h * (h ")) ) by Def3, Def5;
then ( (h ") * (h * g) = f or g * (1_ G) = f * (h * (h ")) ) by Def4, Def5;
then ( ((h ") * h) * g = f or g = f * (h * (h ")) ) by Def3, Def4;
then ( ((h ") * h) * g = f or g = f * (1_ G) ) by Def5;
then ( (1_ G) * g = f or g = f ) by Def4, Def5;
hence g = f by Def4; :: thesis: verum