let G be finite Group; :: thesis: for H being Subgroup of G st card G = card H holds

multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)

let H be Subgroup of G; :: thesis: ( card G = card H implies multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) )

assume A1: card G = card H ; :: thesis: multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)

A2: the carrier of H c= the carrier of G by Def5;

the carrier of H = the carrier of G

multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)

let H be Subgroup of G; :: thesis: ( card G = card H implies multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) )

assume A1: card G = card H ; :: thesis: multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)

A2: the carrier of H c= the carrier of G by Def5;

the carrier of H = the carrier of G

proof

hence
multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)
by Th61; :: thesis: verum
assume
the carrier of H <> the carrier of G
; :: thesis: contradiction

then the carrier of H c< the carrier of G by A2;

hence contradiction by A1, CARD_2:48; :: thesis: verum

end;then the carrier of H c< the carrier of G by A2;

hence contradiction by A1, CARD_2:48; :: thesis: verum