theorem :: GROUP_1A:14

for G being addGroup
for g, h being Element of G ex f being Element of G st g + f = h