let G be addGroup; :: thesis: 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 #)
let H1, H2 be Subgroup of G; :: thesis: ( the carrier of H1 = the carrier of H2 implies addMagma(# the carrier of H1, the addF of H1 #) = addMagma(# the carrier of H2, the addF of H2 #) )
assume the carrier of H1 = the carrier of H2 ; :: thesis: addMagma(# the carrier of H1, the addF of H1 #) = addMagma(# the carrier of H2, the addF of H2 #)
then ( H1 is Subgroup of H2 & H2 is Subgroup of H1 ) by Th57;
hence addMagma(# the carrier of H1, the addF of H1 #) = addMagma(# the carrier of H2, the addF of H2 #) by Th55; :: thesis: verum