let O be set ; :: thesis: for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st H1 * H2 = H2 * H1 holds
the carrier of (H1 "\/" H2) = H1 * H2
let G be GroupWithOperators of O; :: thesis: for H1, H2 being StableSubgroup of G st H1 * H2 = H2 * H1 holds
the carrier of (H1 "\/" H2) = H1 * H2
let H1, H2 be StableSubgroup 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 StableSubgroup of G such that
A1: the carrier of H = (carr H1) * (carr H2) by Th17;

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

set A = (carr H1) \/ (carr H2);
let a be Element of G; :: thesis: ( a in H implies a in H1 "\/" H2 )
set X = { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } ;
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 and
A4: c in carr H2 ;

A5: now :: thesis: for Y being set st Y in { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } holds
a in Y

let Y be set ; :: thesis: ( Y in { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } implies a in Y )
assume Y in { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } ; :: thesis: a in Y
then consider B being Subset of G such that
A6: Y = B and
A7: ex H being strict StableSubgroup of G st
( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) ;
consider H9 being strict StableSubgroup of G such that
A8: B = the carrier of H9 and
A9: (carr H1) \/ (carr H2) c= carr H9 by A7;
c in (carr H1) \/ (carr H2) by A4, XBOOLE_0:def 3;
then A10: c in H9 by A9, STRUCT_0:def 5;
A11: H9 is Subgroup of G by Def7;
b in (carr H1) \/ (carr H2) by A3, XBOOLE_0:def 3;
then b in H9 by A9, STRUCT_0:def 5;
then b * c in H9 by A11, A10, GROUP_2:50;
hence a in Y by A2, A6, A8, STRUCT_0:def 5; :: thesis: verum

end;

carr ((Omega). G) in { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } ;
then a in meet { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } by A5, SETFAM_1:def 1;
then a in the carrier of (the_stable_subgroup_of ((carr H1) \/ (carr H2))) by Th27;
hence a in H1 "\/" H2 by STRUCT_0:def 5; :: thesis: verum

end;

then H is StableSubgroup of H1 "\/" H2 by Th13;
then H is Subgroup of H1 "\/" H2 by Def7;
then A12: the carrier of H c= the carrier of (H1 "\/" H2) by GROUP_2:def 5;
(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 A13: 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 A13, XBOOLE_0:def 3;

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

1_ G in H2 by Lm17;
then A15: 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 A14, A15; :: thesis: verum

end;

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

1_ G in H1 by Lm17;
then A17: 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 A16, A17; :: thesis: verum

end;

end;

end;

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

end;

then H1 "\/" H2 is StableSubgroup of H by A1, Def26;
then H1 "\/" H2 is Subgroup of H by Def7;
then the carrier of (H1 "\/" H2) c= the carrier of H by GROUP_2:def 5;
hence the carrier of (H1 "\/" H2) = H1 * H2 by A1, A12, XBOOLE_0:def 10; :: thesis: verum