for G1, G2 being addGroup st G1 is Subgroup of G2 & G2 is Subgroup of G1 holds
addMagma(# the carrier of G1, the addF of G1 #) = addMagma(# the carrier of G2, the addF of G2 #)