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 ;
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 ;
then A10: c in H9 by ;
A11: H9 is Subgroup of G by Def7;
b in (carr H1) \/ (carr H2) by ;
then b in H9 by ;
then b * c in H9 by ;
hence a in Y by ; :: thesis: verum
end;
carr () 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 ;
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 ;
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 ; :: 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 ; :: thesis: verum
end;
end;
end;
hence x in (carr H1) * (carr H2) ; :: thesis: verum
end;
then H1 "\/" H2 is StableSubgroup of H by ;
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 ; :: thesis: verum