for G being addGroup
for H1, H2 being Subgroup of G st ( for g being Element of G holds
( g in H1 iff g in H2 ) ) holds
addMagma(# the carrier of H1, the addF of H1 #) = addMagma(# the carrier of H2, the addF of H2 #)