let G be Group; :: thesis: for H being Subgroup of G st H is Subgroup of (1). G holds
multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of ((1). G), the multF of ((1). G) #)
let H be Subgroup of G; :: thesis: ( H is Subgroup of (1). G implies multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of ((1). G), the multF of ((1). G) #) )
assume H is Subgroup of (1). G ; :: thesis: multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of ((1). G), the multF of ((1). G) #)
then ( H is Subgroup of (1). G & (1). G is Subgroup of H ) by GROUP_2:65;
hence multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of ((1). G), the multF of ((1). G) #) by GROUP_2:55; :: thesis: verum