let G be Group; :: thesis: 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 )
let H1, N1, H2, N2 be Subgroup of G; :: thesis: ( 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 #) implies ( H1 * N1 = H2 * N2 & H1 /\ N1 = H2 /\ N2 ) )
assume A1: multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) ; :: thesis: ( not multMagma(# the carrier of N1, the multF of N1 #) = multMagma(# the carrier of N2, the multF of N2 #) or ( H1 * N1 = H2 * N2 & H1 /\ N1 = H2 /\ N2 ) )
assume A2: multMagma(# the carrier of N1, the multF of N1 #) = multMagma(# the carrier of N2, the multF of N2 #) ; :: thesis: ( H1 * N1 = H2 * N2 & H1 /\ N1 = H2 /\ N2 )
reconsider K = G as Subgroup of G by GROUP_2:54;
reconsider HK = multMagma(# the carrier of H1, the multF of H1 #), NK = multMagma(# the carrier of N1, the multF of N1 #) as Subgroup of K by Th1;
thus H1 * N1 = HK * NK by ThProdLemma
.= H2 * N2 by A1, A2, ThProdLemma ; :: thesis: H1 /\ N1 = H2 /\ N2
thus H1 /\ N1 = HK /\ NK by ThCapLemma
.= H2 /\ N2 by A1, A2, ThCapLemma ; :: thesis: verum