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) )

assume A1: (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)

A8: H1 is Subgroup of G by Def7;

hence ex H being strict StableSubgroup of G st the carrier of H = (carr H1) * (carr H2) by A17, A9, A2, Lm14; :: thesis: verum

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) )

assume A1: (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)

A2: now :: thesis: for o being Element of O

for g being Element of G st g in (carr H1) * (carr H2) holds

(G ^ o) . g in (carr H1) * (carr H2)

A7:
H2 is Subgroup of G
by Def7;for g being Element of G st g in (carr H1) * (carr H2) holds

(G ^ o) . g in (carr H1) * (carr H2)

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

A3: g = a * b and

A4: a in carr H1 and

A5: b in carr H2 ;

a in H1 by A4, STRUCT_0:def 5;

then (G ^ o) . a in H1 by Lm9;

then A6: (G ^ o) . a in carr H1 by STRUCT_0:def 5;

b in H2 by A5, STRUCT_0:def 5;

then (G ^ o) . b in H2 by Lm9;

then (G ^ o) . b in carr H2 by STRUCT_0:def 5;

then ((G ^ o) . a) * ((G ^ o) . b) in (carr H1) * (carr H2) by A6;

hence (G ^ o) . g in (carr H1) * (carr H2) by A3, GROUP_6:def 6; :: thesis: verum

end;(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

A3: g = a * b and

A4: a in carr H1 and

A5: b in carr H2 ;

a in H1 by A4, STRUCT_0:def 5;

then (G ^ o) . a in H1 by Lm9;

then A6: (G ^ o) . a in carr H1 by STRUCT_0:def 5;

b in H2 by A5, STRUCT_0:def 5;

then (G ^ o) . b in H2 by Lm9;

then (G ^ o) . b in carr H2 by STRUCT_0:def 5;

then ((G ^ o) . a) * ((G ^ o) . b) in (carr H1) * (carr H2) by A6;

hence (G ^ o) . g in (carr H1) * (carr H2) by A3, GROUP_6:def 6; :: thesis: verum

A8: H1 is Subgroup of G by Def7;

A9: now :: thesis: for g being Element of G st g in (carr H1) * (carr H2) holds

g " in (carr H1) * (carr H2)

g " in (carr H1) * (carr H2)

let g be Element of G; :: thesis: ( g in (carr H1) * (carr H2) implies g " in (carr H1) * (carr H2) )

assume A10: g in (carr H1) * (carr H2) ; :: thesis: g " in (carr H1) * (carr H2)

then consider a, b being Element of G such that

A11: g = a * b and

a in carr H1 and

b in carr H2 ;

consider b1, a1 being Element of G such that

A12: a * b = b1 * a1 and

A13: b1 in carr H2 and

A14: a1 in carr H1 by A1, A10, A11;

b1 in H2 by A13, STRUCT_0:def 5;

then b1 " in H2 by A7, GROUP_2:51;

then A15: b1 " in carr H2 by STRUCT_0:def 5;

a1 in H1 by A14, STRUCT_0:def 5;

then a1 " in H1 by A8, GROUP_2:51;

then A16: a1 " in carr H1 by STRUCT_0:def 5;

g " = (a1 ") * (b1 ") by A11, A12, GROUP_1:17;

hence g " in (carr H1) * (carr H2) by A16, A15; :: thesis: verum

end;assume A10: g in (carr H1) * (carr H2) ; :: thesis: g " in (carr H1) * (carr H2)

then consider a, b being Element of G such that

A11: g = a * b and

a in carr H1 and

b in carr H2 ;

consider b1, a1 being Element of G such that

A12: a * b = b1 * a1 and

A13: b1 in carr H2 and

A14: a1 in carr H1 by A1, A10, A11;

b1 in H2 by A13, STRUCT_0:def 5;

then b1 " in H2 by A7, GROUP_2:51;

then A15: b1 " in carr H2 by STRUCT_0:def 5;

a1 in H1 by A14, STRUCT_0:def 5;

then a1 " in H1 by A8, GROUP_2:51;

then A16: a1 " in carr H1 by STRUCT_0:def 5;

g " = (a1 ") * (b1 ") by A11, A12, GROUP_1:17;

hence g " in (carr H1) * (carr H2) by A16, A15; :: thesis: verum

A17: now :: thesis: for g1, g2 being Element of G st g1 in (carr H1) * (carr H2) & g2 in (carr H1) * (carr H2) holds

g1 * g2 in (carr H1) * (carr H2)

(carr H1) * (carr H2) <> {}
by GROUP_2:9;g1 * g2 in (carr H1) * (carr H2)

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

A18: g1 in (carr H1) * (carr H2) and

A19: g2 in (carr H1) * (carr H2) ; :: thesis: g1 * g2 in (carr H1) * (carr H2)

consider a1, b1 being Element of G such that

A20: g1 = a1 * b1 and

A21: a1 in carr H1 and

A22: b1 in carr H2 by A18;

consider a2, b2 being Element of G such that

A23: g2 = a2 * b2 and

A24: a2 in carr H1 and

A25: b2 in carr H2 by A19;

b1 * a2 in (carr H1) * (carr H2) by A1, A22, A24;

then consider a, b being Element of G such that

A26: b1 * a2 = a * b and

A27: a in carr H1 and

A28: b in carr H2 ;

A29: a in H1 by A27, STRUCT_0:def 5;

A30: b in H2 by A28, STRUCT_0:def 5;

b2 in H2 by A25, STRUCT_0:def 5;

then b * b2 in H2 by A7, A30, GROUP_2:50;

then A31: b * b2 in carr H2 by STRUCT_0:def 5;

a1 in H1 by A21, STRUCT_0:def 5;

then a1 * a in H1 by A8, A29, GROUP_2:50;

then A32: a1 * a in carr H1 by STRUCT_0:def 5;

g1 * g2 = ((a1 * b1) * a2) * b2 by A20, A23, GROUP_1:def 3

.= (a1 * (b1 * a2)) * b2 by GROUP_1:def 3 ;

then g1 * g2 = ((a1 * a) * b) * b2 by A26, GROUP_1:def 3

.= (a1 * a) * (b * b2) by GROUP_1:def 3 ;

hence g1 * g2 in (carr H1) * (carr H2) by A32, A31; :: thesis: verum

end;assume that

A18: g1 in (carr H1) * (carr H2) and

A19: g2 in (carr H1) * (carr H2) ; :: thesis: g1 * g2 in (carr H1) * (carr H2)

consider a1, b1 being Element of G such that

A20: g1 = a1 * b1 and

A21: a1 in carr H1 and

A22: b1 in carr H2 by A18;

consider a2, b2 being Element of G such that

A23: g2 = a2 * b2 and

A24: a2 in carr H1 and

A25: b2 in carr H2 by A19;

b1 * a2 in (carr H1) * (carr H2) by A1, A22, A24;

then consider a, b being Element of G such that

A26: b1 * a2 = a * b and

A27: a in carr H1 and

A28: b in carr H2 ;

A29: a in H1 by A27, STRUCT_0:def 5;

A30: b in H2 by A28, STRUCT_0:def 5;

b2 in H2 by A25, STRUCT_0:def 5;

then b * b2 in H2 by A7, A30, GROUP_2:50;

then A31: b * b2 in carr H2 by STRUCT_0:def 5;

a1 in H1 by A21, STRUCT_0:def 5;

then a1 * a in H1 by A8, A29, GROUP_2:50;

then A32: a1 * a in carr H1 by STRUCT_0:def 5;

g1 * g2 = ((a1 * b1) * a2) * b2 by A20, A23, GROUP_1:def 3

.= (a1 * (b1 * a2)) * b2 by GROUP_1:def 3 ;

then g1 * g2 = ((a1 * a) * b) * b2 by A26, GROUP_1:def 3

.= (a1 * a) * (b * b2) by GROUP_1:def 3 ;

hence g1 * g2 in (carr H1) * (carr H2) by A32, A31; :: thesis: verum

hence ex H being strict StableSubgroup of G st the carrier of H = (carr H1) * (carr H2) by A17, A9, A2, Lm14; :: thesis: verum