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