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:78;

now :: thesis: for a being Element of G st a in H holds
a in H1 "\/" H2

reconsider p = 1 as Integer ;
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
A2: a = b * c and
A3: ( b in carr H1 & c in carr H2 ) ;
( b in (carr H1) \/ (carr H2) & c in (carr H1) \/ (carr H2) ) by A3, XBOOLE_0:def 3;
then A4: ( rng <*b,c*> = {b,c} & {b,c} c= (carr H1) \/ (carr H2) ) by FINSEQ_2:127, ZFMISC_1:32;
A5: ( len <*b,c*> = 2 & len <*(@ p),(@ p)*> = 2 ) by FINSEQ_1:44;
a = (Product <*b*>) * c by A2, FINSOP_1:11
.= (Product <*b*>) * (Product <*c*>) by FINSOP_1:11
.= Product (<*b*> ^ <*c*>) by FINSOP_1:5
.= Product <*b,c*> by FINSEQ_1:def 9
.= Product <*(b |^ p),c*> by GROUP_1:26
.= Product <*(b |^ p),(c |^ p)*> by GROUP_1:26
.= Product (<*b,c*> |^ <*(@ p),(@ p)*>) by Th23 ;
hence a in H1 "\/" H2 by A5, A4, Th28; :: thesis: verum

end;

then A6: H is Subgroup of H1 "\/" H2 by GROUP_2:58;
(carr H1) \/ (carr H2) c= (carr H1) * (carr H2)

proof

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

now :: thesis: x in (carr H1) * (carr H2)

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

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

1_ G in H2 by GROUP_2:46;
then A9: 1_ G in carr H2 by STRUCT_0:def 5;
a * (1_ G) = a by GROUP_1:def 4;
hence x in (carr H1) * (carr H2) by A8, A9; :: thesis: verum

end;

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

1_ G in H1 by GROUP_2:46;
then A11: 1_ G in carr H1 by STRUCT_0:def 5;
(1_ G) * a = a by GROUP_1:def 4;
hence x in (carr H1) * (carr H2) by A10, A11; :: thesis: verum

end;

end;

end;

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

end;

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