let G be addGroup; :: 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 RLVECT_1:def 3;
then ( (- h) + (h + g) = (0_ G) + f or g + (h + (- h)) = f + (h + (- h)) ) by RLVECT_1:def 3, Def5;
then ( (- h) + (h + g) = f or g + (0_ G) = f + (h + (- h)) ) by Def4, Def5;
then ( ((- h) + h) + g = f or g = f + (h + (- h)) ) by RLVECT_1:def 3, Def4;
then ( ((- h) + h) + g = f or g = f + (0_ G) ) by Def5;
then ( (0_ G) + g = f or g = f ) by Def4, Def5;
hence g = f by Def4; :: thesis: verum