theorem Th61: :: GROUP_1A:107

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 #)