for G being addGroup
for f, g, h being Element of G holds
( f + h = g iff f = g + (- h) )