theorem :: GROUP_1A:119

for G being finite addGroup
for H being Subgroup of G st card G = card H holds
addMagma(# the carrier of H, the addF of H #) = addMagma(# the carrier of G, the addF of G #)