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 ) ) by STRUCT_0:def 5;
G is Subgroup of G by Th63;
hence multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) by A1, Th69; :: thesis: verum