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