let G be Group; :: thesis: for H1, H2 being Subgroup of G st H1 * H2 = H2 * H1 holds
the carrier of (H1 "\/" H2) = H1 * H2
let H1, H2 be Subgroup of G; :: thesis: ( H1 * H2 = H2 * H1 implies the carrier of (H1 "\/" H2) = H1 * H2 )
assume H1 * H2 = H2 * H1 ; :: thesis: the carrier of (H1 "\/" H2) = H1 * H2
then consider H being strict Subgroup of G such that
A1: the carrier of H = (carr H1) * (carr H2) by GROUP_2:93;
(carr H1) \/ (carr H2) c= (carr H1) * (carr H2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (carr H1) \/ (carr H2) or x in (carr H1) * (carr H2) )
assume A2: x in (carr H1) \/ (carr H2) ; :: thesis: x in (carr H1) * (carr H2)
then reconsider a = x as Element of G ;

now

per cases ( x in carr H1 or x in carr H2 ) by A2, XBOOLE_0:def 3;

suppose A3: x in carr H1 ; :: thesis: x in (carr H1) * (carr H2)

1_ G in H2 by GROUP_2:55;
then ( 1_ G in carr H2 & a * (1_ G) = a ) by GROUP_1:def 5, STRUCT_0:def 5;
hence x in (carr H1) * (carr H2) by A3; :: thesis: verum

end;

suppose A4: x in carr H2 ; :: thesis: x in (carr H1) * (carr H2)

1_ G in H1 by GROUP_2:55;
then ( 1_ G in carr H1 & (1_ G) * a = a ) by GROUP_1:def 5, STRUCT_0:def 5;
hence x in (carr H1) * (carr H2) by A4; :: thesis: verum

end;

end;

end;

hence x in (carr H1) * (carr H2) ; :: thesis: verum

end;

then A5: H1 "\/" H2 is Subgroup of H by A1, Def5;

now

let a be Element of G; :: thesis: ( a in H implies a in H1 "\/" H2 )
assume a in H ; :: thesis: a in H1 "\/" H2
then a in (carr H1) * (carr H2) by A1, STRUCT_0:def 5;
then consider b, c being Element of G such that
A6: a = b * c and
A7: ( b in carr H1 & c in carr H2 ) ;
reconsider p = 1 as Integer ;
A8: ( len <*b,c*> = 2 & len <*(@ p),(@ p)*> = 2 ) by FINSEQ_1:61;
A9: rng <*b,c*> = {b,c} by FINSEQ_2:147;
( b in (carr H1) \/ (carr H2) & c in (carr H1) \/ (carr H2) ) by A7, XBOOLE_0:def 3;
then A10: {b,c} c= (carr H1) \/ (carr H2) by ZFMISC_1:38;
a = (Product <*b*>) * c by A6, FINSOP_1:12
.= (Product <*b*>) * (Product <*c*>) by FINSOP_1:12
.= Product (<*b*> ^ <*c*>) by Th8
.= Product <*b,c*> by FINSEQ_1:def 9
.= Product <*(b |^ p),c*> by GROUP_1:44
.= Product <*(b |^ p),(c |^ p)*> by GROUP_1:44
.= Product (<*b,c*> |^ <*(@ p),(@ p)*>) by Th29 ;
hence a in H1 "\/" H2 by A8, A9, A10, Th37; :: thesis: verum

end;

then H is Subgroup of H1 "\/" H2 by GROUP_2:67;
hence the carrier of (H1 "\/" H2) = H1 * H2 by A1, A5, GROUP_2:64; :: thesis: verum