let G be addGroup; :: thesis: for H being Subgroup of G st ( for g being Element of G holds g in 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: ( ( for g being Element of G holds g in H ) implies addMagma(# the carrier of H, the addF of H #) = addMagma(# the carrier of G, the addF of G #) )
assume for g being Element of G holds g in H ; :: thesis: addMagma(# the carrier of H, the addF of H #) = addMagma(# the carrier of G, the addF of G #)
then A1: for g being Element of G holds
( ( g in H implies g in G ) & ( g in G implies g in H ) ) ;
G is Subgroup of G by ThA54;
hence addMagma(# the carrier of H, the addF of H #) = addMagma(# the carrier of G, the addF of G #) by A1, Th60; :: thesis: verum