for G being non empty addGroup-like addMagma
for g1, g2 being Element of G
for H being Subgroup of G
for h1, h2 being Element of H st h1 = g1 & h2 = g2 holds
h1 + h2 = g1 + g2