let O be set ; :: thesis: for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st (carr H1) * (carr H2) = (carr H2) * (carr H1) holds
ex H being strict StableSubgroup of G st the carrier of H = (carr H1) * (carr H2)
let G be GroupWithOperators of O; :: thesis: for H1, H2 being StableSubgroup of G st (carr H1) * (carr H2) = (carr H2) * (carr H1) holds
ex H being strict StableSubgroup of G st the carrier of H = (carr H1) * (carr H2)
let H1, H2 be StableSubgroup of G; :: thesis: ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict StableSubgroup of G st the carrier of H = (carr H1) * (carr H2) )
A1: ( H1 is Subgroup of G & H2 is Subgroup of G ) by Def7;
assume A2: (carr H1) * (carr H2) = (carr H2) * (carr H1) ; :: thesis: ex H being strict StableSubgroup of G st the carrier of H = (carr H1) * (carr H2)
A3: (carr H1) * (carr H2) <> {} by GROUP_2:13;

A4: now

let g1, g2 be Element of G; :: thesis: ( g1 in (carr H1) * (carr H2) & g2 in (carr H1) * (carr H2) implies g1 * g2 in (carr H1) * (carr H2) )
assume that
A5: g1 in (carr H1) * (carr H2) and
A6: g2 in (carr H1) * (carr H2) ; :: thesis: g1 * g2 in (carr H1) * (carr H2)
consider a1, b1 being Element of G such that
A7: ( g1 = a1 * b1 & a1 in carr H1 & b1 in carr H2 ) by A5;
consider a2, b2 being Element of G such that
A8: ( g2 = a2 * b2 & a2 in carr H1 & b2 in carr H2 ) by A6;
A9: g1 * g2 = ((a1 * b1) * a2) * b2 by A7, A8, GROUP_1:def 4
.= (a1 * (b1 * a2)) * b2 by GROUP_1:def 4 ;
b1 * a2 in (carr H1) * (carr H2) by A2, A7, A8;
then consider a, b being Element of G such that
A10: ( b1 * a2 = a * b & a in carr H1 & b in carr H2 ) ;
A11: g1 * g2 = ((a1 * a) * b) * b2 by A9, A10, GROUP_1:def 4
.= (a1 * a) * (b * b2) by GROUP_1:def 4 ;
( a1 in H1 & a in H1 ) by A7, A10, STRUCT_0:def 5;
then a1 * a in H1 by A1, GROUP_2:59;
then A12: a1 * a in carr H1 by STRUCT_0:def 5;
( b2 in H2 & b in H2 ) by A8, A10, STRUCT_0:def 5;
then b * b2 in H2 by A1, GROUP_2:59;
then b * b2 in carr H2 by STRUCT_0:def 5;
hence g1 * g2 in (carr H1) * (carr H2) by A11, A12; :: thesis: verum

end;

A13: now

let g be Element of G; :: thesis: ( g in (carr H1) * (carr H2) implies g " in (carr H1) * (carr H2) )
assume A14: g in (carr H1) * (carr H2) ; :: thesis: g " in (carr H1) * (carr H2)
then consider a, b being Element of G such that
A15: ( g = a * b & a in carr H1 & b in carr H2 ) ;
consider b1, a1 being Element of G such that
A16: ( a * b = b1 * a1 & b1 in carr H2 & a1 in carr H1 ) by A2, A14, A15;
A17: g " = (a1 " ) * (b1 " ) by A15, A16, GROUP_1:25;
( b1 in H2 & a1 in H1 ) by A16, STRUCT_0:def 5;
then ( b1 " in H2 & a1 " in H1 ) by A1, GROUP_2:60;
then ( a1 " in carr H1 & b1 " in carr H2 ) by STRUCT_0:def 5;
hence g " in (carr H1) * (carr H2) by A17; :: thesis: verum

end;

now

let o be Element of O; :: thesis: for g being Element of G st g in (carr H1) * (carr H2) holds
(G ^ o) . g in (carr H1) * (carr H2)
let g be Element of G; :: thesis: ( g in (carr H1) * (carr H2) implies (G ^ o) . g in (carr H1) * (carr H2) )
assume g in (carr H1) * (carr H2) ; :: thesis: (G ^ o) . g in (carr H1) * (carr H2)
then consider a, b being Element of G such that
A18: ( g = a * b & a in carr H1 & b in carr H2 ) ;
( b in H2 & a in H1 ) by A18, STRUCT_0:def 5;
then ( (G ^ o) . b in H2 & (G ^ o) . a in H1 ) by Lm10;
then ( (G ^ o) . b in carr H2 & (G ^ o) . a in carr H1 ) by STRUCT_0:def 5;
then ((G ^ o) . a) * ((G ^ o) . b) in (carr H1) * (carr H2) ;
hence (G ^ o) . g in (carr H1) * (carr H2) by A18, GROUP_6:def 7; :: thesis: verum

end;

hence ex H being strict StableSubgroup of G st the carrier of H = (carr H1) * (carr H2) by A3, A4, A13, Lm15; :: thesis: verum