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