let G be finite addGroup; :: thesis: 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 #)
let H be Subgroup of G; :: thesis: ( card G = card H implies addMagma(# the carrier of H, the addF of H #) = addMagma(# the carrier of G, the addF of G #) )
assume A1: card G = card H ; :: thesis: addMagma(# the carrier of H, the addF of H #) = addMagma(# the carrier of G, the addF of G #)
the carrier of H = the carrier of G
proof
assume the carrier of H <> the carrier of G ; :: thesis: contradiction
then the carrier of H c< the carrier of G by DefA5;
hence contradiction by A1, CARD_2:48; :: thesis: verum
end;
hence addMagma(# the carrier of H, the addF of H #) = addMagma(# the carrier of G, the addF of G #) by Th61; :: thesis: verum