theorem Th42: :: GROUP_24:16

for G being Group
for H1, N1, H2, N2 being Subgroup of G st multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) & multMagma(# the carrier of N1, the multF of N1 #) = multMagma(# the carrier of N2, the multF of N2 #) holds
( H1 * N1 = H2 * N2 & H1 /\ N1 = H2 /\ N2 )