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

assume for g being Element of G holds g in H ; :: thesis: multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)

then A1: for g being Element of G holds

( ( g in H implies g in G ) & ( g in G implies g in H ) ) ;

G is Subgroup of G by Th54;

hence multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) by A1, Th60; :: 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: ( ( for g being Element of G holds g in H ) implies multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) )

assume for g being Element of G holds g in H ; :: thesis: multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)

then A1: for g being Element of G holds

( ( g in H implies g in G ) & ( g in G implies g in H ) ) ;

G is Subgroup of G by Th54;

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