theorem ThProdLemma: :: GROUP_24:7

for G being Group
for H1, H2, K being Subgroup of G
for K1, K2 being Subgroup of K st multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of K1, the multF of K1 #) & multMagma(# the carrier of H2, the multF of H2 #) = multMagma(# the carrier of K2, the multF of K2 #) holds
H1 * H2 = K1 * K2