let G be Group; 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; ( ( 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 )
; 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; verum