let G be Group; :: thesis: for H1, H2 being Subgroup of G st ( for g being Element of G holds

( g in H1 iff g in H2 ) ) holds

multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)

let H1, H2 be Subgroup of G; :: thesis: ( ( for g being Element of G holds

( g in H1 iff g in H2 ) ) implies multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) )

assume for g being Element of G holds

( g in H1 iff g in H2 ) ; :: thesis: multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)

then ( H1 is Subgroup of H2 & H2 is Subgroup of H1 ) by Th58;

hence multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) by Th55; :: thesis: verum

( g in H1 iff g in H2 ) ) holds

multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)

let H1, H2 be Subgroup of G; :: thesis: ( ( for g being Element of G holds

( g in H1 iff g in H2 ) ) implies multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) )

assume for g being Element of G holds

( g in H1 iff g in H2 ) ; :: thesis: multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)

then ( H1 is Subgroup of H2 & H2 is Subgroup of H1 ) by Th58;

hence multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) by Th55; :: thesis: verum