let G be Group; :: thesis: for H being Subgroup of G st the carrier of G c= the carrier of 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: ( the carrier of G c= the carrier of H implies multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) )

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

A2: G is Subgroup of G by Th54;

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

then the carrier of G = the carrier of H by A1;

hence multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) by A2, Th59; :: thesis: verum

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: ( the carrier of G c= the carrier of H implies multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) )

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

A2: G is Subgroup of G by Th54;

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

then the carrier of G = the carrier of H by A1;

hence multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) by A2, Th59; :: thesis: verum