let G be addGroup; :: thesis: 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 #)
let H be Subgroup of G; :: thesis: ( the carrier of G c= the carrier of H implies addMagma(# the carrier of H, the addF of H #) = addMagma(# the carrier of G, the addF of G #) )
assume A1: the carrier of G c= the carrier of H ; :: thesis: addMagma(# the carrier of H, the addF of H #) = addMagma(# the carrier of G, the addF of G #)
A2: G is Subgroup of G by ThA54;
the carrier of G = the carrier of H by A1, DefA5;
hence addMagma(# the carrier of H, the addF of H #) = addMagma(# the carrier of G, the addF of G #) by A2, Th59; :: thesis: verum