let G be Group; :: thesis: 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
let H1, H2, K be Subgroup of G; :: thesis: 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
let K1, K2 be Subgroup of K; :: thesis: ( 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 #) implies H1 * H2 = K1 * K2 )
assume A1: multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of K1, the multF of K1 #) ; :: thesis: ( not multMagma(# the carrier of H2, the multF of H2 #) = multMagma(# the carrier of K2, the multF of K2 #) or H1 * H2 = K1 * K2 )
assume A2: multMagma(# the carrier of H2, the multF of H2 #) = multMagma(# the carrier of K2, the multF of K2 #) ; :: thesis: H1 * H2 = K1 * K2
A3: carr H1 = carr K1 by A1;
A4: carr H2 = carr K2 by A2;
for x being object holds
( x in (carr H1) * (carr H2) iff x in (carr K1) * (carr K2) )

proof

let x be object ; :: thesis: ( x in (carr H1) * (carr H2) iff x in (carr K1) * (carr K2) )
thus ( x in (carr H1) * (carr H2) implies x in (carr K1) * (carr K2) ) :: thesis: ( x in (carr K1) * (carr K2) implies x in (carr H1) * (carr H2) )

proof

assume x in (carr H1) * (carr H2) ; :: thesis: x in (carr K1) * (carr K2)
then consider h1, h2 being Element of G such that
B1: ( x = h1 * h2 & h1 in carr H1 & h2 in carr H2 ) ;
reconsider k1 = h1, k2 = h2 as Element of K by A3, A4, B1;
k1 * k2 = x by B1, GROUP_2:43;
hence x in (carr K1) * (carr K2) by A3, A4, B1; :: thesis: verum

end;

assume x in (carr K1) * (carr K2) ; :: thesis: x in (carr H1) * (carr H2)
then consider k1, k2 being Element of K such that
B1: ( x = k1 * k2 & k1 in carr K1 & k2 in carr K2 ) ;
reconsider h1 = k1, h2 = k2 as Element of G by GROUP_2:42;
h1 * h2 = x by B1, GROUP_2:43;
hence x in (carr H1) * (carr H2) by A3, A4, B1; :: thesis: verum

end;

then A5: (carr H1) * (carr H2) = (carr K1) * (carr K2) by TARSKI:2;
thus H1 * H2 = (carr H1) * (carr H2) by GROUP_4:def 8
.= K1 * K2 by A5, GROUP_4:def 8 ; :: thesis: verum